normedCommRing — Mathlib

English

A subalgebra of a normed commutative ring is itself a normed commutative ring by restricting the norm.

Русский

Подалгебра нормированного коммутативного кольца образует нормированное кольцо по ограничению нормы.

LaTeX

$$$\text{If } s \text{ is a Subalgebra of a NormedCommRing } E, \; s \text{ is a NormedCommRing with restricted norm.}$$$

Lean4

/-- A subalgebra of a normed commutative ring is also a normed commutative ring, with the
restriction of the norm. -/
instance normedCommRing {𝕜 : Type*} [CommRing 𝕜] {E : Type*} [NormedCommRing E] [Algebra 𝕜 E] (s : Subalgebra 𝕜 E) :
    NormedCommRing s :=
  { s.seminormedCommRing, s.normedRing with }

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