Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-14 09:33 05d87671

View on Github →

feat(group_theory/order_of_element): additivize (#10766)

Estimated changes

Modified src/algebra/pointwise.lean

Modified src/group_theory/order_of_element.lean

deleted theorem add_order_of_eq_prime

modified theorem commute.order_of_mul_dvd_lcm

deleted theorem commute.order_of_mul_dvd_lcm_order_of

deleted theorem image_range_add_order_of

deleted theorem is_of_fin_add_order_iff_nsmul_eq_zero

deleted theorem is_periodic_pt_add_iff_nsmul_eq_zero

added theorem mem_powers_iff_mem_range_order_of'

modified def pow_coprime

modified theorem pow_coprime_inv

modified theorem pow_coprime_one