mathlib3

912f195f - feat(dynamics/periodic_pts): Lemma about periodic point from periodic point of iterate (#12940)