Commit 2023-01-27 16:09 97e5cdb7

View on Github →

feat: port Dynamics.PeriodicPts (#1887)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Int/Basic.lean

Modified Mathlib/Dynamics/FixedPoints/Basic.lean

Created Mathlib/Dynamics/PeriodicPts.lean

added theorem Function.Commute.minimalPeriod_of_comp_dvd_lcm

added theorem Function.Commute.minimalPeriod_of_comp_dvd_mul

added theorem Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime

added theorem Function.IsFixedPt.isPeriodicPt

added theorem Function.IsPeriodicPt.apply_iterate

added theorem Function.IsPeriodicPt.comp

added theorem Function.IsPeriodicPt.comp_lcm

added theorem Function.IsPeriodicPt.eq_of_apply_eq

added theorem Function.IsPeriodicPt.eq_of_apply_eq_same

added theorem Function.IsPeriodicPt.eq_zero_of_lt_minimalPeriod

added theorem Function.IsPeriodicPt.iterate_mod_apply

added theorem Function.IsPeriodicPt.left_of_add

added theorem Function.IsPeriodicPt.left_of_comp

added theorem Function.IsPeriodicPt.minimalPeriod_dvd

added theorem Function.IsPeriodicPt.minimalPeriod_le

added theorem Function.IsPeriodicPt.minimalPeriod_pos

added theorem Function.IsPeriodicPt.right_of_add

added theorem Function.IsPeriodicPt.trans_dvd

added def Function.IsPeriodicPt

added theorem Function.Semiconj.mapsTo_periodicPts

added theorem Function.Semiconj.mapsTo_ptsOfPeriod

added theorem Function.bUnion_ptsOfPeriod

added theorem Function.bijOn_periodicPts

added theorem Function.bijOn_ptsOfPeriod

added theorem Function.directed_ptsOfPeriod_pNat

added theorem Function.eq_iff_lt_minimalPeriod_of_iterate_eq

added theorem Function.eq_of_lt_minimalPeriod_of_iterate_eq

added theorem Function.isPeriodicPt_iff_minimalPeriod_dvd

added theorem Function.isPeriodicPt_minimalPeriod

added theorem Function.isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate

added theorem Function.isPeriodicPt_zero

added theorem Function.is_fixed_point_iff_minimalPeriod_eq_one

added theorem Function.is_periodic_id

added theorem Function.iterate_add_minimalPeriod_eq

added theorem Function.iterate_mem_periodicOrbit

added theorem Function.iterate_minimalPeriod

added theorem Function.iterate_mod_minimalPeriod_eq

added theorem Function.le_of_lt_minimalPeriod_of_iterate_eq

added theorem Function.mem_periodicOrbit_iff

added theorem Function.mem_periodicPts

added theorem Function.mem_ptsOfPeriod

added def Function.minimalPeriod

added theorem Function.minimalPeriod_apply

added theorem Function.minimalPeriod_apply_iterate

added theorem Function.minimalPeriod_eq_minimalPeriod_iff

added theorem Function.minimalPeriod_eq_prime

added theorem Function.minimalPeriod_eq_prime_pow

added theorem Function.minimalPeriod_eq_zero_iff_nmem_periodicPts

added theorem Function.minimalPeriod_eq_zero_of_nmem_periodicPts

added theorem Function.minimalPeriod_id

added theorem Function.minimalPeriod_iterate_eq_div_gcd'

added theorem Function.minimalPeriod_iterate_eq_div_gcd

added theorem Function.minimalPeriod_pos_iff_mem_periodicPts

added theorem Function.minimalPeriod_pos_of_mem_periodicPts

added theorem Function.mk_mem_periodicPts

added theorem Function.nodup_periodicOrbit

added theorem Function.not_isPeriodicPt_of_pos_of_lt_minimalPeriod

added def Function.periodicOrbit

added theorem Function.periodicOrbit_apply_eq

added theorem Function.periodicOrbit_apply_iterate_eq

added theorem Function.periodicOrbit_chain'

added theorem Function.periodicOrbit_chain

added theorem Function.periodicOrbit_def

added theorem Function.periodicOrbit_eq_cycle_map

added theorem Function.periodicOrbit_eq_nil_iff_not_periodic_pt

added theorem Function.periodicOrbit_eq_nil_of_not_periodic_pt

added theorem Function.periodicOrbit_length

added def Function.periodicPts

added def Function.ptsOfPeriod

added theorem Function.self_mem_periodicOrbit

added theorem Function.unionᵢ_pNat_ptsOfPeriod

added theorem MulAction.pow_smul_eq_iff_minimalPeriod_dvd

added theorem MulAction.pow_smul_mod_minimalPeriod

added theorem MulAction.zpow_smul_eq_iff_minimalPeriod_dvd

added theorem MulAction.zpow_smul_mod_minimalPeriod