Rings with open units: the inverse #
A topological monoid M has open units (IsOpenUnits M) when Units.val : Mˣ → M is an open
embedding: the units are open and inversion is continuous on them for the subspace topology.
In a monoid with zero with open units, Ring.inverse is therefore continuous at every unit.
Main declarations #
IsOpenUnits.continuousAt_ringInverse:Ring.inverseis continuous at every unit of a ring with open units.
theorem
IsOpenUnits.continuousAt_ringInverse
{R : Type u_1}
[MonoidWithZero R]
[TopologicalSpace R]
[IsOpenUnits R]
(u : Rˣ)
:
In a monoid with zero whose units are open with continuous inversion, Ring.inverse is
continuous at every unit.