Commit 2023-07-16 11:35 dcf4f619

View on Github →

chore: forward port leanprover-community/mathlib#18719 (#5936)

Estimated changes

Modified Mathlib/Data/Prod/Basic.lean

Modified Mathlib/Dynamics/PeriodicPts.lean

added theorem Function.isFixedPt_prod_map

added theorem Function.isPeriodicPt_prod_map

added theorem Function.iterate_prod_map

added theorem Function.minimalPeriod_fst_dvd

added theorem Function.minimalPeriod_prod_map

added theorem Function.minimalPeriod_snd_dvd

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem IsOfFinOrder.fst

added theorem IsOfFinOrder.mono

added theorem IsOfFinOrder.prod_mk

added theorem IsOfFinOrder.snd

modified theorem MonoidHom.isOfFinOrder

added theorem injective_zpow_iff_not_isOfFinOrder

added theorem orderOf_fst_dvd_orderOf

added theorem orderOf_snd_dvd_orderOf

added theorem zpow_eq_one_iff_modEq

added theorem zpow_eq_zpow_iff_modEq