toRingSeminorm — Mathlib

English

The norm on a NormedRing can be regarded as a RingNorm on that ring.

Русский

Норма на нормированном кольце может рассматриваться как RingNorm на этом кольце.

LaTeX

$$$(\text{NormedRing.toRingNorm } R) \in \text{RingNorm } R$$$

Lean4

/-- The seminorm on a `SeminormedRing`, as a `RingSeminorm`. -/
def toRingSeminorm (R : Type*) [SeminormedRing R] : RingSeminorm R
    where
  toFun := norm
  map_zero' := norm_zero
  add_le' := norm_add_le
  mul_le' := norm_mul_le
  neg' := norm_neg

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