Commit 2025-07-24 14:37 d349b440

View on Github →

chore: move DiscreteUniformity lower in the import tree (#27384)

Estimated changes

Modified Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

added theorem DiscreteUniformity.eq_pure_cauchyConst

added theorem DiscreteUniformity.eq_pure_of_cauchy

Modified Mathlib/Topology/UniformSpace/DiscreteUniformity.lean

deleted theorem DiscreteUniformity.eq_pure_cauchyConst

deleted theorem DiscreteUniformity.eq_pure_of_cauchy