imK_intCast — Mathlib

English

Let z be an integer. When z is viewed in the quaternion algebra ℍ[R], its K-coordinate is zero; i.e., the K-imaginary part vanishes.

Русский

Пусть z — целое число. Рассматривая z как элемент алгебры кватернионов ℍ[R], его компонент вдоль оси k равна нулю; т. е. imK(z) = 0.

LaTeX

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

Lean4

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

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