Structures · Topology
IsTopologicalDivisionRing
A topological division ring is a division ring with a topology where all operations are continuous, including inversion.
- Defined in
- Mathlib.Topology.Algebra.Field
- Shape
- One type argument
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Real
- UniformSpace.Completion
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- Subfield.topologicalClosure
- UniformSpace.Completion.hatInv_extends
- Subfield.le_topologicalClosure
- Subfield.isClosed_topologicalClosure
- UniformSpace.Completion.instField
- IsTopologicalDivisionRing.toIsTopologicalRing
- UniformSpace.Completion.mul_hatInv_cancel
- Subfield.topologicalClosure_minimal
- Subfield.topologicalClosure.congr_simp
- IsTopologicalDivisionRing.toContinuousInv₀
- UniformSpace.Completion.instIsTopologicalDivisionRing
- completableTopField_of_complete
- UniformSpace.Completion.coe_inv