normSq_ratCast

Mathlib.Algebra.Quaternion

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

English

For any rational q, normSq(q) equals q^2 in the quaternion algebra.

Русский

Для рационального q норма квадрата равна q^2 в кватернионной алгебре.

LaTeX

$$$\operatorname{normSq}(q) = q^{2}$ for $q \in \mathbb{Q}$ embedded into $\mathbb{H}(R)$$$

Lean4

@[norm_cast]
theorem normSq_ratCast (q : ℚ) : normSq (q : ℍ[R]) = (q : ℍ[R]) ^ 2 := by rw [← coe_ratCast, normSq_coe, coe_pow]

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

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

Разделы

Аффилиация

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