Commit 2024-02-17 03:41 1a7456e3

View on Github →

feat: several results about Monoid.Exponent (#9975)

Estimated changes

Modified Mathlib/GroupTheory/Exponent.lean

added theorem Commute.of_orderOf_dvd_two

added theorem Group.exponent_dvd_card

added theorem Group.exponent_dvd_nat_card

modified theorem Group.one_lt_exponent

added theorem Monoid.ExponentExists.isOfFinOrder

added theorem Monoid.ExponentExists.of_finite

added theorem Monoid.ExponentExists.orderOf_pos

added theorem Monoid.exists_orderOf_eq_exponent

modified theorem Monoid.exponentExists_iff_ne_zero

added theorem Monoid.exponent_dvd

added theorem Monoid.exponent_dvd_iff_forall_pow_eq_one

added theorem Monoid.exponent_dvd_of_forall_orderOf_dvd

deleted theorem Monoid.exponent_dvd_of_forall_pow_eq_one

modified theorem Monoid.exponent_eq_zero_iff

added theorem Monoid.exponent_ne_zero

modified theorem Monoid.exponent_ne_zero_of_finite

added theorem Monoid.exponent_pos

added theorem Monoid.lcm_orderOf_eq_exponent

deleted theorem Monoid.lcm_order_eq_exponent

added theorem Monoid.orderOf_le_exponent

added def commMonoidOfExponentTwo

added def instCommGroupOfExponentTwo

added theorem inv_eq_self_of_exponent_two

added theorem inv_eq_self_of_orderOf_eq_two

added theorem mul_comm_of_exponent_two

added theorem mul_not_mem_of_exponent_two

added theorem mul_not_mem_of_orderOf_eq_two

added theorem orderOf_eq_two_iff

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/GroupTheory/SpecificGroups/KleinFour.lean

deleted def instCommGroupOfExponentTwo

deleted theorem inv_eq_self_of_exponent_two

deleted theorem inv_eq_self_of_orderOf_eq_two

deleted theorem mul_comm_of_exponent_two

deleted theorem mul_not_mem_of_exponent_two

deleted theorem mul_not_mem_of_orderOf_eq_two

deleted theorem orderOf_eq_two_iff

Modified Mathlib/GroupTheory/Torsion.lean