English
A subalgebra of a seminormed ring inherits a seminormed ring structure by restricting the norm.
Русский
Подалгебра полуправила нормированного кольца наследует структуру полуморного кольца за счет ограничения нормы.
LaTeX
$$$\text{Let } S \text{ be a subalgebra of a seminormed ring } E. \text{ Then } S \text{ is a SeminormedRing with the restricted norm: } \|x\|_{S} = \|x\|_{E}. $$$
Lean4
/-- A subalgebra of a seminormed ring is also a seminormed ring, with the restriction of the
norm. -/
instance seminormedRing {𝕜 : Type*} [CommRing 𝕜] {E : Type*} [SeminormedRing E] [Algebra 𝕜 E] (s : Subalgebra 𝕜 E) :
SeminormedRing s :=
{ s.toSubmodule.seminormedAddCommGroup, s.toRing with norm_mul_le a b := norm_mul_le a.1 b.1 }
