seminorm_one_eq_one_iff_ne_zero — Mathlib

English

Let p be a ring seminorm on a ring R with p(1) ≤ 1. Then p(1) = 1 if and only if p ≠ 0.

Русский

Пусть p — кольцевой семинорм на кольце R и p(1) ≤ 1. Тогда p(1) = 1 тогда же, когда p ≠ 0.

LaTeX

$$$ p(1) \le 1 \;\Rightarrow\; p(1) = 1 \iff p \neq 0 $$$

Lean4

theorem seminorm_one_eq_one_iff_ne_zero (hp : p 1 ≤ 1) : p 1 = 1 ↔ p ≠ 0 :=
  by
  refine ⟨fun h => ne_zero_iff.mpr ⟨1, by rw [h]; exact one_ne_zero⟩, fun h => ?_⟩
  obtain hp0 | hp0 := (apply_nonneg p (1 : R)).eq_or_lt'
  · exfalso
    refine h (ext fun x => (apply_nonneg _ _).antisymm' ?_)
    simpa only [hp0, mul_one, mul_zero] using map_mul_le_mul p x 1
  · refine hp.antisymm ((le_mul_iff_one_le_left hp0).1 ?_)
    simpa only [one_mul] using map_mul_le_mul p (1 : R) _

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