sq_eq_normSq

Mathlib.Algebra.Quaternion

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

← MathLib Explorer

English

normSq (a + b) equals normSq a plus normSq b plus the cross-term involving a and b.

Русский

normSq(a+b) = normSq(a) + normSq(b) + перекрестный член с a и b.

LaTeX

$$normSq(a + b) = normSq(a) + normSq(b) + 2 * (a * star b).re$$

Lean4

theorem sq_eq_normSq : a ^ 2 = normSq a ↔ a = a.re :=
  by
  rw [← star_eq_self, ← star_mul_self, sq, mul_eq_mul_right_iff, eq_comm]
  exact or_iff_left_of_imp fun ha ↦ ha.symm ▸ star_zero _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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