English
A non-unital subalgebra class of a non-unital seminormed ring is itself a non-unital seminormed ring with restricted norm.
Русский
Класс неединичного подполья над неединичным seminormedRing сам образует неединичный seminormedRing с ограниченной нормой.
LaTeX
$$$\text{Instance } nonUnitalSeminormedRing {S} {E} (s:S) : NonUnitalSeminormedRing s$$$
Lean4
/-- A non-unital subalgebra of a non-unital seminormed ring is also a non-unital 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) nonUnitalSeminormedRing {S 𝕜 E : Type*} [CommRing 𝕜] [NonUnitalSeminormedRing E] [Module 𝕜 E]
[SetLike S E] [NonUnitalSubringClass S E] [SMulMemClass S 𝕜 E] (s : S) : NonUnitalSeminormedRing s :=
{ AddSubgroupClass.seminormedAddCommGroup s, NonUnitalSubringClass.toNonUnitalRing s with
norm_mul_le a b := norm_mul_le a.1 b.1 }
