normSq_coe

Mathlib.Algebra.Quaternion

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

English

For x in the base ring, normSq(x) equals x^2 when x is embedded as a quaternion.

Русский

Для x из основания норма^2(x) равна x^2, когда x встроено как кватернион.

LaTeX

$$$ normSq (x) = x^2 $$$

Lean4

theorem normSq_coe : normSq (x : ℍ[R]) = x ^ 2 := by rw [normSq_def, star_coe, ← coe_mul, re_coe, sq]

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

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

Разделы

Аффилиация

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