norm_one — Mathlib

English

In a C*-ring, the norm of the multiplicative unit is 1, provided the ring is nontrivial.

Русский

В C*-кольце норма единицы равна 1, при условии непустоты кольца.

LaTeX

$$$ \|1_E\| = 1 $$$

Lean4

theorem norm_one [Nontrivial E] : ‖(1 : E)‖ = 1 :=
  by
  have : 0 < ‖(1 : E)‖ := norm_pos_iff.mpr one_ne_zero
  rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]
    -- see Note [lower instance priority]

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