English
A nonunital subalgebra of a nonunital normed commutative ring is itself a nonunital seminormed commutative ring with the norm restricted to the subalgebra.
Русский
Неединичная подалгебра из неединичного нормированного коммутативного кольца сама образует неединичное семинормированное коммутативное кольцо с ограниченной нормой.
LaTeX
$$$\text{If } s \subseteq E \text{ is a nonUnitalSubalgebra and } E \text{ is a nonUnital NormedCommRing},\; s \text{ inherits a nonUnital SeminormedCommRing structure via restriction of norm.}$$$
Lean4
/-- A non-unital subalgebra of a non-unital seminormed commutative ring is also a non-unital
seminormed commutative ring, with the restriction of the norm. -/
instance nonUnitalSeminormedCommRing {𝕜 : Type*} [CommRing 𝕜] {E : Type*} [NonUnitalSeminormedCommRing E] [Module 𝕜 E]
(s : NonUnitalSubalgebra 𝕜 E) : NonUnitalSeminormedCommRing s :=
{ s.nonUnitalSeminormedRing, s.toNonUnitalCommRing with }
