Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 13:11 e8386bd4

View on Github →

feat(group_theory/exponent): Define the exponent of a group (#10249) This PR provides the definition and some very basic API for the exponent of a group/monoid.

Estimated changes

Modified src/algebra/gcd_monoid/finset.lean

added theorem finset.lcm_eq_zero_iff

Modified src/algebra/gcd_monoid/multiset.lean

added theorem multiset.lcm_eq_zero_iff

Created src/group_theory/exponent.lean

added theorem monoid.exp_eq_one_of_subsingleton

added theorem monoid.exponent_dvd_of_forall_pow_eq_one

added def monoid.exponent_exists

added theorem monoid.exponent_min'

added theorem monoid.exponent_min

added theorem monoid.exponent_pos_of_exists

added theorem monoid.lcm_order_eq_exponent

added theorem monoid.lcm_order_of_dvd_exponent

added theorem monoid.order_dvd_exponent

added theorem monoid.pow_eq_mod_exponent

added theorem monoid.pow_exponent_eq_one