toRingNorm — Mathlib

English

For a NormedRing R, the RingNorm obtained from the norm satisfies equality with the standard norm: (NormedRing.toRingNorm R) x = ||x||.

Русский

Для NormedRing R нормированная структура RingNorm даёт равенство: (NormedRing.toRingNorm R) x = ||x||.

LaTeX

$$$(\text{NormedRing.toRingNorm } R)\, x = \|x\|$$$

Lean4

/-- The norm on a `NormedRing`, as a `RingNorm`. -/
@[simps]
def toRingNorm (R : Type*) [NormedRing R] : RingNorm R
    where
  toFun := norm
  map_zero' := norm_zero
  add_le' := norm_add_le
  mul_le' := norm_mul_le
  neg' := norm_neg
  eq_zero_of_map_eq_zero' x hx := by rw [← norm_eq_zero]; exact hx

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