Commit 2025-01-21 06:54 a52aa033

View on Github →

chore(Topology/Instances/Real): reduce imports (#20548)

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Quotient.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/Topology/Instances/Real/Defs.lean

added theorem Real.uniformContinuous_const_mul

Modified Mathlib/Topology/Instances/Real/Lemmas.lean

deleted theorem Real.uniformContinuous_const_mul