Normed rings #
In this file we continue building the theory of (semi)normed rings.
Non-unital seminormed ring structure on the product of finitely many non-unital seminormed rings, using the sup norm.
Equations
- One or more equations did not get rendered due to their size.
Seminormed ring structure on the product of finitely many seminormed rings, using the sup norm.
Equations
- One or more equations did not get rendered due to their size.
If σ
and σ'
are mutually inverse, then one is RingHomIsometric
if the other is. Not an
instance, as it would cause loops.
Normed ring structure on the product of finitely many non-unital normed rings, using the sup norm.
Equations
- One or more equations did not get rendered due to their size.
Normed ring structure on the product of finitely many normed rings, using the sup norm.
Equations
- One or more equations did not get rendered due to their size.
Non-unital seminormed commutative ring structure on the product of finitely many non-unital seminormed commutative rings, using the sup norm.
Equations
- Pi.nonUnitalSeminormedCommRing = { toNonUnitalSeminormedRing := Pi.nonUnitalSeminormedRing, mul_comm := ⋯ }
Normed commutative ring structure on the product of finitely many non-unital normed commutative rings, using the sup norm.
Equations
- One or more equations did not get rendered due to their size.
Seminormed commutative ring structure on the product of finitely many seminormed commutative rings, using the sup norm.
Equations
- One or more equations did not get rendered due to their size.
Normed commutative ring structure on the product of finitely many normed commutative rings, using the sup norm.
Equations
- One or more equations did not get rendered due to their size.
A seminormed ring is a topological ring.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- SeparationQuotient.instNormedRing = { toNorm := NormedAddCommGroup.toNorm, toRing := inferInstance, toMetricSpace := NormedAddCommGroup.toMetricSpace, dist_eq := ⋯, norm_mul_le := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Multiplication by a nonzero element a
on the left, as a Dilation
of a ring with a strictly
multiplicative norm.
Equations
- Dilation.mulLeft a ha = { toFun := fun (b : α) => a * b, edist_eq' := ⋯ }
Instances For
Multiplication by a nonzero element a
on the right, as a Dilation
of a ring with a strictly
multiplicative norm.
Equations
- Dilation.mulRight a ha = { toFun := fun (b : α) => b * a, edist_eq' := ⋯ }