toNormOneClass — Mathlib

English

From a NormMulClass on a nontrivial normed ring, one can deduce a NormOneClass structure by defining norm(1) = 1.

Русский

Из NormMulClass на не тривиальном нормированном кольце выводят NormOneClass, задавая norm(1)=1.

LaTeX

$$$\\text{norm}(1)=1$$$

Lean4

/-- Deduce `NormOneClass` from `NormMulClass` under a suitable nontriviality hypothesis. Not
an instance, in order to avoid loops with `NormOneClass.nontrivial`. -/
theorem toNormOneClass : NormOneClass α where
  norm_one := by
    obtain ⟨u, hu⟩ := exists_ne (0 : α)
    simpa [mul_eq_left₀ (norm_ne_zero_iff.mpr hu)] using (norm_mul u 1).symm

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