Structures · Topology

CompletableTopField

A topological field is completable if it is separated and the image under the mapping x ↦ x⁻¹ of every Cauchy filter (with respect to the additive uniform structure) which does not have a cluster point at 0 is a Cauchy filter (with respect to the additive uniform structure). This ensures the completion is a field.

Defined in

Mathlib.Topology.Algebra.UniformField

Shape

One type argument · adds nice