Commit 2025-04-28 13:45 bff59ee7

View on Github →

chore(PeriodicPts): review API, fix (#24422)

fix some lemma names introduced in #23086;
fix some Fintype/Finite assumptions (found by the linter in #10235);
golf some proofs.

Estimated changes

Modified Mathlib/Dynamics/PeriodicPts/Defs.lean

deleted theorem Function.iUnion_pNat_ptsOfPeriod

added theorem Function.iUnion_pnat_ptsOfPeriod

deleted theorem Function.periodicPts_subset_image

added theorem Function.periodicPts_subset_range

Modified Mathlib/Dynamics/PeriodicPts/Lemmas.lean

added theorem Function.Injective.mem_periodicPts

deleted theorem Function.directed_ptsOfPeriod_pNat

added theorem Function.directed_ptsOfPeriod_pnat

deleted theorem Function.injective_iff_forall_mem_periodicPts

modified theorem Function.injective_iff_iterate_factorial_card_eq_id

added theorem Function.injective_iff_periodicPts_eq_univ

modified theorem Function.isPeriodicPt_factorial_card_of_mem_periodicPts

modified theorem Function.mem_periodicPts_iff_isPeriodicPt_factorial_card

deleted theorem Function.mem_periodicPts_of_injective

modified theorem Function.minimalPeriod_le_card