Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-14 16:30 d07245fd

View on Github →

feat(group_theory/order_of_element): Order in α × β (#18719) The order of (a, b) is the lcm of the orders of a and b. Match pow and zpow lemmas. Also some variables noise because I could not use x to mean what I wanted, and incidentally the type A was mostly unused.

Estimated changes

Modified src/data/prod/basic.lean

modified theorem prod.map_id

Modified src/dynamics/periodic_pts.lean

added theorem function.is_fixed_pt_prod_map

added theorem function.is_periodic_pt_prod_map

added theorem function.iterate_prod_map

added theorem function.minimal_period_fst_dvd

added theorem function.minimal_period_prod_map

added theorem function.minimal_period_snd_dvd

Modified src/group_theory/order_of_element.lean

added theorem injective_zpow_iff_not_is_of_fin_order

added theorem is_of_fin_order.fst

added theorem is_of_fin_order.mono

added theorem is_of_fin_order.prod_mk

added theorem is_of_fin_order.snd

modified theorem monoid_hom.is_of_fin_order

added theorem order_of_fst_dvd_order_of

added theorem order_of_snd_dvd_order_of

added theorem zpow_eq_one_iff_modeq

added theorem zpow_eq_zpow_iff_modeq