Commit 2025-01-18 22:00 bdee03dd

View on Github →

chore(Dynamics/PeriodicPts): don't import MonoidWithZero (#20765) For this, split the file into .Defs and .Lemmas.

Estimated changes

Modified Archive/Imo/Imo2006Q5.lean

Modified Mathlib.lean

Renamed Mathlib/Dynamics/PeriodicPts.lean to Mathlib/Dynamics/PeriodicPts/Defs.lean

deleted theorem Function.Commute.minimalPeriod_of_comp_dvd_mul

deleted theorem Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime

deleted theorem Function.bijOn_periodicPts

deleted theorem Function.directed_ptsOfPeriod_pNat

deleted theorem Function.minimalPeriod_eq_prime

deleted theorem Function.minimalPeriod_eq_prime_pow

deleted theorem Function.minimalPeriod_fst_dvd

deleted theorem Function.minimalPeriod_prod_map

deleted theorem Function.minimalPeriod_snd_dvd

Created Mathlib/Dynamics/PeriodicPts/Lemmas.lean

added theorem Function.Commute.minimalPeriod_of_comp_dvd_mul

added theorem Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime

added theorem Function.bijOn_periodicPts

added theorem Function.directed_ptsOfPeriod_pNat

added theorem Function.minimalPeriod_eq_prime

added theorem Function.minimalPeriod_eq_prime_pow

added theorem Function.minimalPeriod_fst_dvd

added theorem Function.minimalPeriod_prod_map

added theorem Function.minimalPeriod_snd_dvd

Modified Mathlib/GroupTheory/GroupAction/FixedPoints.lean

Modified Mathlib/GroupTheory/GroupAction/Period.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean