English
Let A be a nonunital normed ring and S a nonunital subalgebra of A. Then S inherits a nonunital normed ring structure by restricting the norm to S.
Русский
Пусть A — ненулевое нормированное кольцо без единицы и S — ненулевая подпалгебра A. Тогда S наследует структуру ненульного нормированного кольца за счет ограничения нормы на S.
LaTeX
$$$\text{Let } A \text{ be a nonunital normed ring and } S \le A. \text{ Then } (S, \|\cdot\||_{S}) \text{ is a nonunital normed ring with } \|x\|_{S} = \|x\|_{A} \text{ for } x \in S.$$$
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 nonUnitalNormedRing {𝕜 : Type*} [CommRing 𝕜] {E : Type*} [NonUnitalNormedRing E] [Module 𝕜 E]
(s : NonUnitalSubalgebra 𝕜 E) : NonUnitalNormedRing s :=
{ s.nonUnitalSeminormedRing with eq_of_dist_eq_zero := eq_of_dist_eq_zero }
