English
A nonunital subalgebra of a nonunital normed ring is again a nonunital normed ring under the restricted norm, in a class-setting of subring-like structures.
Русский
Ненулевая подподалгебра ненулевого нормированного кольца снова образует ненулевое нормированное кольцо под ограниченной нормой, в рамках класса подобной подкольцевой структуры.
LaTeX
$$$\text{Let } S \text{ be a set-like nonunital subring class contained in a nonunital normed ring } E. \text{ Then } S \text{ carries a NonUnitalNormedRing structure with } \|x\|_{S} = \|x\|_{E}.$$$
Lean4
/-- A non-unital subalgebra of a non-unital normed ring is also a non-unital normed ring,
with the restriction of the norm. -/
instance (priority := 75) nonUnitalNormedRing {S 𝕜 E : Type*} [CommRing 𝕜] [NonUnitalNormedRing E] [Module 𝕜 E]
[SetLike S E] [NonUnitalSubringClass S E] [SMulMemClass S 𝕜 E] (s : S) : NonUnitalNormedRing s :=
{ nonUnitalSeminormedRing s with eq_of_dist_eq_zero := eq_of_dist_eq_zero }
