Commit 2025-03-31 10:57 e0c2dbd5

View on Github →

feat(Mathlib/Dynamics/PeriodicPts/Lemmas): Added lemmas about periodicPts on Fintype (#23086)

Estimated changes

Modified Mathlib/Dynamics/PeriodicPts/Defs.lean

added theorem Function.periodicPts_subset_image

Modified Mathlib/Dynamics/PeriodicPts/Lemmas.lean

added theorem Function.injective_iff_forall_mem_periodicPts

added theorem Function.injective_iff_iterate_factorial_card_eq_id

added theorem Function.isPeriodicPt_factorial_card_of_mem_periodicPts

added theorem Function.mem_periodicPts_iff_isPeriodicPt_factorial_card

added theorem Function.mem_periodicPts_of_injective

added theorem Function.minimalPeriod_le_card