normSq_natCast

Mathlib.Algebra.Quaternion

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

English

For a natural number n, normSq(n) = n^2 when n is viewed as a quaternion.

Русский

Для натурального числа n, normSq(n) = n^2, если рассматривать n как кватернион.

LaTeX

$$$ normSq (n : \mathbb{H}(R)) = (n : R)^2 $$$

Lean4

@[norm_cast]
theorem normSq_natCast (n : ℕ) : normSq (n : ℍ[R]) = (n : R) ^ 2 := by rw [← coe_natCast, normSq_coe]

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

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

Разделы

Аффилиация

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