Commit 2022-04-25 11:19 ad0a3e66

View on Github →

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.

Estimated changes

Modified src/dynamics/periodic_pts.lean

added theorem function.iterate_injective_of_lt_minimal_period

added theorem function.iterate_minimal_period

Modified src/group_theory/order_of_element.lean

deleted theorem pow_injective_aux