fact: Definition isTopological_ConstructiveField (X : ConstructiveField) (is : isTopologicalSpace X) := isTopological_ring X is × continuous_on (U := (pr111 X) ,, is) (V := (pr111 X) ,, is) (λ x : X, (x ≠ 0)%CF) CFinv.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures