Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-10 07:36 39184f40

View on Github →

feat(dynamics/periodic_pts): Orbit under periodic function (#12976)

Estimated changes

Modified src/dynamics/periodic_pts.lean

added theorem function.eq_iff_lt_minimal_period_of_iterate_eq

added theorem function.eq_of_lt_minimal_period_of_iterate_eq

modified theorem function.is_periodic_pt.minimal_period_dvd

modified theorem function.is_periodic_pt_iff_minimal_period_dvd

modified theorem function.is_periodic_pt_minimal_period

added theorem function.iterate_add_minimal_period_eq

deleted theorem function.iterate_eq_mod_minimal_period

deleted theorem function.iterate_injective_of_lt_minimal_period

added theorem function.iterate_mem_periodic_orbit

modified theorem function.iterate_minimal_period

added theorem function.iterate_mod_minimal_period_eq

added theorem function.le_of_lt_minimal_period_of_iterate_eq

added theorem function.mem_periodic_orbit_iff

added theorem function.minimal_period_apply

added theorem function.minimal_period_apply_iterate

added theorem function.minimal_period_eq_zero_iff_nmem_periodic_pts

added theorem function.minimal_period_eq_zero_of_nmem_periodic_pts

added theorem function.nodup_periodic_orbit

added def function.periodic_orbit

added theorem function.periodic_orbit_apply_eq

added theorem function.periodic_orbit_apply_iterate_eq

added theorem function.periodic_orbit_def

added theorem function.periodic_orbit_eq_cycle_map

added theorem function.periodic_orbit_eq_nil_iff_not_periodic_pt

added theorem function.periodic_orbit_eq_nil_of_not_periodic_pt

added theorem function.periodic_orbit_length

added theorem function.self_mem_periodic_orbit

Modified src/group_theory/order_of_element.lean