English
In a subalgebra with the restricted norm, zero distance implies equality of points: if d_S(x,y) = 0 then x = y.
Русский
В подподалгебре с ограниченной нормой нулевое расстояние означает тождественную эквивалентность точек: если d_S(x,y) = 0, то x = y.
LaTeX
$$$\forall x,y \in S,\ d_S(x,y)=0 \Rightarrow x=y.$$$
Lean4
/-- A subalgebra of a seminormed ring is also a seminormed ring, with the restriction of the
norm. -/
-- necessary to require `SMulMemClass S 𝕜 E` so that `𝕜` can be determined as an `outParam`
@[nolint unusedArguments]
instance (priority := 75) seminormedRing {S 𝕜 E : Type*} [CommRing 𝕜] [SeminormedRing E] [Algebra 𝕜 E] [SetLike S E]
[SubringClass S E] [SMulMemClass S 𝕜 E] (s : S) : SeminormedRing s :=
{ AddSubgroupClass.seminormedAddCommGroup s, SubringClass.toRing s with norm_mul_le a b := norm_mul_le a.1 b.1 }
