toNormedRing — Mathlib

English

MulRingSeminorm is equipped with a functional-like structure, i.e., its coercion to functions behaves like a function.

Русский

MulRingSeminorm имеет структурy, подобную функции, то есть преобразование в функцию ведёт себя как функция.

LaTeX

$$$\text{MulRingSeminorm\,R} \text{ has a FunLike structure on } R$$$

Lean4

/-- The `NormedRing` structure on a ring `R` determined by a `RingNorm` -/
-- See note |reducible non-instances]

abbrev toNormedRing [Ring R] (f : RingNorm R) : NormedRing R
    where
  __ := ‹Ring R›
  __ := f.toAddGroupNorm.toNormedAddCommGroup
  norm_mul_le := map_mul_le_mul f

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