im_sq — Mathlib

English

For any quaternion a, the square of its imaginary part equals the negative of the norm of that imaginary part: (a.im)^2 = - normSq(a.im).

Русский

Для любого квартониона a квадрат мнимой части равен минус квадрат нормы этой мнимой части: (a.im)^2 = -normSq(a.im).

LaTeX

$$$(a.im)^2 = -\operatorname{normSq}(a.im)$$$

Lean4

theorem im_sq : a.im ^ 2 = -normSq a.im := by simp_rw [sq, ← star_mul_self, star_im, neg_mul, neg_neg]

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