im_intCast

Mathlib.Algebra.Quaternion

URI: https://scilib.ai/kg/mathlib#Quaternion.im_intCast

English

Let z be an integer. The i-coordinate (im) of z in ℍ[R] is zero.

Русский

Пусть z — целое число. Компонента вдоль оси i (im) элемента z в ℍ[R] равна нулю.

LaTeX

$$$\\forall z \\in \\mathbb{Z}, (z : \\mathbb{H}(R)).\\mathrm{im} = 0$$$

Lean4

@[simp, norm_cast]
theorem im_intCast (z : ℤ) : (z : ℍ[R]).im = 0 :=
  rfl

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru