instNormOneClassOfNontrivial — Mathlib

English

If E is a nontrivial normed ring with star and C*-structure, then E carries a NormOneClass structure (norm of 1 equals 1).

Русский

Если E — ненулевое нормированное кольцо с операцией звезды и структурой C*-кольца, то E обладает структурой NormOneClass (норма единицы равна 1).

LaTeX

$$NormOneClass E$$

Lean4

instance (priority := 100) [Nontrivial E] : NormOneClass E :=
  ⟨norm_one⟩

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