Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-01 18:49 d8de5672

View on Github →

feat(group_theory/order_of_element): generalised to add_order_of (#6770) This PR defines add_order_of for an additive monoid. If someone sees how to do this with more automation, let me know. This gets one step towards closing issue #1563. Coauthored by: Yakov Pechersky @pechersky

Estimated changes

added theorem of_add_eq_one
added theorem of_mul_eq_zero
added theorem of_mul_gpow
added theorem of_mul_pow
added theorem gcd_nsmul_eq_zero
added theorem add_order_of_eq_prime
added theorem add_order_of_eq_zero
added theorem add_order_of_injective
added theorem add_order_of_nsmul''
added theorem add_order_of_nsmul'
added theorem add_order_of_nsmul
added theorem add_order_of_pos'
added theorem add_order_of_pos
added theorem add_order_of_zero
added theorem card_nsmul_eq_zero
added theorem exists_gsmul_eq_zero
added theorem exists_nsmul_eq_zero
added theorem nsmul_injective_aux
modified theorem order_of_eq_prime_pow
modified theorem order_of_le_card_univ
modified theorem order_of_pos
modified theorem order_of_subgroup
modified theorem order_of_submonoid
added theorem pow_injective_aux