sq_eq_neg_normSq — Mathlib

English

For a quaternion a, a^2 = normSq(a) if and only if a equals its real part a.re (i.e., a is real).

Русский

Для квартониона a верно: a^2 = normSq(a) тогда и только тогда, когда a = a.re (то есть a вещественный).

LaTeX

$$a^2 = \operatorname{normSq}(a) \iff a = a.re$$

Lean4

theorem sq_eq_neg_normSq : a ^ 2 = -normSq a ↔ a.re = 0 :=
  by
  simp_rw [← star_eq_neg]
  obtain rfl | hq0 := eq_or_ne a 0
  · simp
  · rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]

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