English
Every nonzero ring seminorm on a field K gives rise to a RingNorm on K.
Русский
У всякой ненулевой кольцевой семинормы на поле K образуется кольцевая норма на K.
LaTeX
$$$\text{toRingNorm}(f,\mathrm{hnt}) \in \text{RingNorm}(K)$$$
Lean4
/-- A nonzero ring seminorm on a field `K` is a ring norm. -/
def toRingNorm {K : Type*} [Field K] (f : RingSeminorm K) (hnt : f ≠ 0) : RingNorm K :=
{ f with
eq_zero_of_map_eq_zero' := fun x hx =>
by
obtain ⟨c, hc⟩ := RingSeminorm.ne_zero_iff.mp hnt
by_contra hn0
have hc0 : f c = 0 :=
by
rw [← mul_one c, ← mul_inv_cancel₀ hn0, ← mul_assoc, mul_comm c, mul_assoc]
exact
le_antisymm
(le_trans (map_mul_le_mul f _ _)
(by rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx, zero_mul]))
(apply_nonneg f _)
exact hc hc0 }
