norm_star — Mathlib

English

The norm is preserved by the quaternion conjugation (star): ∥star a∥ = ∥a∥ for all a ∈ ℍ.

Русский

Норма сохраняется под звездочкой (конъугированием): ∥star a∥ = ∥a∥ для всех a ∈ ℍ.

LaTeX

$$$\\|\\star a\\| = \\|a\\| \\quad (a \\in \\mathbb{H}).$$$

Lean4

theorem norm_star (a : ℍ) : ‖star a‖ = ‖a‖ := by
  simp_rw [norm_eq_sqrt_real_inner, inner_self, normSq_star]
    -- This does not need to be `@[simp]`, as it is a consequence of later simp lemmas.

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