to_normOneClass — Mathlib

English

In a normed division ring with discrete topology, for any x, ||x|| = 1 if and only if x ≠ 0.

Русский

В нормированном делении кольца с дискретной топологией для любого x выполнено: ||x|| = 1 тогда и только тогда, когда x ≠ 0.

LaTeX

$$$\|x\| = 1 \iff x \neq 0$$$

Lean4

instance (priority := 900) to_normOneClass : NormOneClass α :=
  ⟨mul_left_cancel₀ (mt norm_eq_zero.1 (one_ne_zero' α)) <| by rw [← norm_mul, mul_one, mul_one]⟩

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