Commit 2024-10-29 06:30 7bf29018

View on Github →

chore: split Topology.Instances.Real (#18370)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Affine/AddTorsor.lean

Modified Mathlib/Analysis/Subadditive.lean

Modified Mathlib/NumberTheory/Modular.lean

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

Modified Mathlib/Topology/Instances/AddCircle.lean

Modified Mathlib/Topology/Instances/CantorSet.lean

Modified Mathlib/Topology/Instances/NNReal.lean

Modified Mathlib/Topology/Instances/Real.lean

deleted theorem AddSubgroup.tendsto_zmultiples_subtype_cofinite

deleted theorem Int.tendsto_coe_cofinite

deleted theorem Int.tendsto_zmultiplesHom_cofinite

Created Mathlib/Topology/Instances/ZMultiples.lean

added theorem AddSubgroup.tendsto_zmultiples_subtype_cofinite

added theorem Int.tendsto_coe_cofinite

added theorem Int.tendsto_zmultiplesHom_cofinite

Modified Mathlib/Topology/Order/Bounded.lean

Modified Mathlib/Topology/UniformSpace/CompareReals.lean