Commit 2025-12-07 22:10 466925b9

View on Github →

feat(Dynamics/PeriodicPts): some theorems for Pi.map in Dynamics/PeriodicPts analogous to those for Prod.map (#29530) Split from #29204. Some namespace prefixes are added in GroupTheory/OrderOfElement.lean to distinguish the extra imports introduced.

depends on: #29528

Estimated changes

Modified Mathlib/Dynamics/PeriodicPts/Defs.lean

added theorem Function.IsFixedPt.piMap

added theorem Function.IsPeriodicPt.piMap

added theorem Function.isFixedPt_piMap

added theorem Function.isPeriodicPt_piMap

Modified Mathlib/Dynamics/PeriodicPts/Lemmas.lean

added theorem Function.minimalPeriod_eq_sInf_n_pos_IsPeriodicPt

added theorem Function.minimalPeriod_piMap

added theorem Function.minimalPeriod_piMap_fintype

added theorem Function.minimalPeriod_single_dvd_minimalPeriod_piMap

Modified Mathlib/GroupTheory/OrderOfElement.lean

modified theorem orderOf_pow'

modified theorem orderOf_pow

modified theorem pow_gcd_card_eq_one_iff