mathlib3

ad0a3e66 - feat(dynamics/periodic_pts): Iteration is injective below the period (#13660)

feat(dynamics/periodic_pts): Iteration is injective below the period (#13660) This PR adds `iterate_injective_of_lt_minimal_period`, generalizing `pow_injective_of_lt_order_of`.