Commit 2023-04-07 11:23 875c586d

View on Github →

feat: port Topology.Algebra.UniformField (#3049)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/UniformField.lean

added theorem UniformSpace.Completion.coe_inv

added theorem UniformSpace.Completion.continuous_hatInv

added def UniformSpace.Completion.hatInv

added theorem UniformSpace.Completion.hatInv_extends

added theorem UniformSpace.Completion.mul_hatInv_cancel