Commit 2025-06-06 12:02 fda802e3

View on Github →

refactor(Topology/Instances): split AddCircle to remove dependence on reals (#25530) This is just a small thing I noticed while prepping a student's work for submission: splitting up the file defining AddCircle, in order to avoid various algebra files having a spurious dependence on path-connectedness.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Grp/Injective.lean

Modified Mathlib/Algebra/Lie/Weights/Chain.lean

Modified Mathlib/Algebra/Module/CharacterModule.lean

Modified Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean

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

Modified Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean

Renamed Mathlib/Topology/Instances/AddCircle.lean to Mathlib/Topology/Instances/AddCircle/Defs.lean

modified theorem AddCircle.coe_fract

deleted theorem ZMod.toAddCircle_apply

deleted theorem ZMod.toAddCircle_eq_zero

deleted theorem ZMod.toAddCircle_inj

deleted theorem ZMod.toAddCircle_injective

deleted theorem ZMod.toAddCircle_intCast

deleted theorem ZMod.toAddCircle_natCast

Modified Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean

Created Mathlib/Topology/Instances/AddCircle/Real.lean

added theorem ZMod.toAddCircle_apply

added theorem ZMod.toAddCircle_eq_zero

added theorem ZMod.toAddCircle_inj

added theorem ZMod.toAddCircle_injective

added theorem ZMod.toAddCircle_intCast

added theorem ZMod.toAddCircle_natCast

Modified scripts/noshake.json