mulRingSeminormClass — Mathlib

English

MulRingSeminormClass is the class of structures mapping 0, 1, addition, and multiplication compatibly into ℝ.

Русский

MulRingSeminormClass — это класс структур, сохраняющих нулевое, единичное элементы, сложение и умножение в ℝ.

LaTeX

$$$\text{MulRingSeminormClass } (MulRingSeminorm R)\, R\, \mathbb{R}$$$

Lean4

instance mulRingSeminormClass : MulRingSeminormClass (MulRingSeminorm R) R ℝ
    where
  map_zero f := f.map_zero'
  map_one f := f.map_one'
  map_add_le_add f := f.add_le'
  map_mul f := f.map_mul'
  map_neg_eq_map f := f.neg'

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