ringNormClass — Mathlib

English

RingNorm R forms a RingNormClass on R with values in ℝ, i.e., it satisfies the axioms of a normed ring structure.

Русский

RingNorm R образует класс RingNorm на кольце R с значениями в ℝ, удовлетворяя аксиомам нормированной структуры кольца.

LaTeX

$$$\text{RingNorm}(R) \text{ is a RingNormClass on } R \text{ with values in } \mathbb{R}$$$

Lean4

instance ringNormClass : RingNormClass (RingNorm R) R ℝ
    where
  map_zero f := f.map_zero'
  map_add_le_add f := f.add_le'
  map_mul_le_mul f := f.mul_le'
  map_neg_eq_map f := f.neg'
  eq_zero_of_map_eq_zero f := f.eq_zero_of_map_eq_zero' _

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