Commit 2025-03-26 23:52 c66c94d8

View on Github →

chore(Topology/Algebra): move defs to new files (#23321)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Floor/Prime.lean

Modified Mathlib/Dynamics/Flow.lean

Modified Mathlib/Topology/Algebra/Affine.lean

Modified Mathlib/Topology/Algebra/Algebra/Rat.lean

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

deleted theorem Continuous.div'

deleted theorem Continuous.inv

deleted theorem ContinuousAt.div'

deleted theorem ContinuousAt.inv

deleted theorem ContinuousOn.div'

deleted theorem ContinuousOn.inv

deleted theorem ContinuousWithinAt.div'

deleted theorem ContinuousWithinAt.inv

deleted theorem Filter.Tendsto.div'

deleted theorem Filter.Tendsto.inv

Created Mathlib/Topology/Algebra/Group/Defs.lean

added theorem Continuous.div'

added theorem Continuous.inv

added theorem ContinuousOn.div'

added theorem ContinuousOn.inv

added theorem ContinuousWithinAt.div'

added theorem Filter.Tendsto.div'

added theorem Filter.Tendsto.inv

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

deleted theorem Continuous.mul

deleted theorem ContinuousAt.mul

deleted theorem ContinuousOn.mul

deleted theorem ContinuousWithinAt.mul

deleted theorem Filter.Tendsto.mul

deleted theorem continuous_mul

Created Mathlib/Topology/Algebra/Monoid/Defs.lean

added theorem Continuous.mul

added theorem ContinuousAt.mul

added theorem ContinuousOn.mul

added theorem ContinuousWithinAt.mul

added theorem Filter.Tendsto.mul

added theorem continuous_mul

Modified Mathlib/Topology/Algebra/Order/Group.lean

Modified Mathlib/Topology/Instances/ENat.lean

Modified Mathlib/Topology/List.lean