normSq — Mathlib

English

The imaginary part changes sign under conjugation: star a.im = - a.im.

Русский

Мнимая часть меняет знак при сопряжении: star a.im = - a.im.

LaTeX

$$$ star a.im = - a.im $$$

Lean4

/-- Square of the norm. -/
def normSq : ℍ[R] →*₀ R where
  toFun a := (a * star a).re
  map_zero' := by simp only [star_zero, zero_mul, re_zero]
  map_one' := by simp only [star_one, one_mul, re_one]
  map_mul' x
    y :=
    coe_injective <| by
      conv_lhs =>
        rw [← mul_star_eq_coe, star_mul, mul_assoc, ← mul_assoc y, y.mul_star_eq_coe, coe_commutes, ← mul_assoc,
          x.mul_star_eq_coe, ← coe_mul]

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