Commit 2023-05-25 14:50 f85a2b8c

View on Github →

feat: port GroupTheory.Exponent (#4313)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Exponent.lean

added def Monoid.ExponentExists

added theorem Monoid.exp_eq_one_of_subsingleton

added theorem Monoid.exponentExists_iff_ne_zero

added theorem Monoid.exponent_dvd_of_forall_pow_eq_one

added theorem Monoid.exponent_eq_iSup_orderOf'

added theorem Monoid.exponent_eq_iSup_orderOf

added theorem Monoid.exponent_eq_max'_orderOf

added theorem Monoid.exponent_eq_zero_iff

added theorem Monoid.exponent_eq_zero_iff_range_orderOf_infinite

added theorem Monoid.exponent_eq_zero_of_order_zero

added theorem Monoid.exponent_min'

added theorem Monoid.exponent_min

added theorem Monoid.exponent_ne_zero_iff_range_orderOf_finite

added theorem Monoid.exponent_ne_zero_of_finite

added theorem Monoid.exponent_pos_of_exists

added theorem Monoid.lcm_orderOf_dvd_exponent

added theorem Monoid.lcm_order_eq_exponent

added theorem Monoid.order_dvd_exponent

added theorem Monoid.pow_eq_mod_exponent

added theorem Monoid.pow_exponent_eq_one

added theorem Nat.Prime.exists_orderOf_eq_pow_factorization_exponent

added theorem card_dvd_exponent_pow_rank'

added theorem card_dvd_exponent_pow_rank