Theorems · Inductive type · field theory
CompletableTopField
(K : Type u_1) → [Field K] → [UniformSpace K] → Prop
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
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- FieldUniformSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement · cited by 7,404
- UniformSpacestatement · cited by 2,040
Cited by7
Results whose statement or proof uses this declaration.
- CompletableTopField.nicestatement and proof · cited by 2
- UniformSpace.Completion.continuous_hatInvstatement and proof · cited by 1
- UniformSpace.Completion.coe_invstatement and proof · cited by 0
- IsUniformInducing.completableTopFieldstatement and proof · cited by 0
- CompletableTopField.casesOnstatement and proof · cited by 0
- CompletableTopField.recOnstatement and proof · cited by 0
- UniformSpace.Completion.mul_hatInv_cancelstatement and proof · cited by 0