star_mul_self

Mathlib.Algebra.Quaternion

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

English

Similarly, the product with the conjugate on the left equals the norm squared: star(a) · a = normSq(a).

Русский

Аналогично, произведение сопряженного слева на само себя дает квадрат нормы: a* · a = normSq(a).

LaTeX

$$$\star a \cdot a = \operatorname{normSq}(a)$$$

Lean4

theorem star_mul_self : star a * a = normSq a := by rw [star_comm_self, self_mul_star]

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

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

Разделы

Аффилиация

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