instL1SeminormedCommRing — Mathlib

English

tsze R M inherits a NormedCommRing structure from R and M when the necessary bounded actions exist.

Русский

tsze R M наследует NormedCommRing структуру от R и M при существовании необходимых ограниченных действий.

LaTeX

$$$\\text{NormedCommRing}(tsze(R,M))$$$

Lean4

instance instL1SeminormedCommRing : SeminormedCommRing (tsze R M)
    where
  __ : CommRing (tsze R M) := inferInstance
  __ : SeminormedRing (tsze R M) := inferInstance

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