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