[Merged by Bors] - feat: several results about Monoid.Exponent

[Ruben-VandeVelde]

---

[j-loreaux]

Yaël is correct, I have provided the proofs. Please remove the extraneous hypothesis. Otherwise LGTM.

[Ruben-VandeVelde]

I've run leaff on this PR, though I don't fully trust the output:

+ added Monoid.exponent_pos.{u}
+ added Monoid.ExponentExists.isOfFinOrder.{u}
+ added AddMonoid.lcm_addOrderOf_eq_exponent.{u}
+ added AddMonoid.ExponentExists.exponent_pos.{u}
+ added AddMonoid.addOrderOf_le_exponent.{u}
+ added Monoid.exponent_dvd_iff_forall_pow_eq_one.{u}
+ added AddMonoid.exists_addOrderOf_eq_exponent.{u}
+ added AddMonoid.ExponentExists.isOfFinAddOrder.{u}
+ added Monoid.ExponentExists.orderOf_pos.{u}
+ added Monoid.ExponentExists.of_finite.{u}
+ added AddMonoid.exponent_dvd_of_forall_addOrderOf_dvd.{u}
+ added commMonoidOfExponentTwo.{u}
+ added Monoid.ExponentExists.exponent_ne_zero.{u}
+ added AddMonoid.ExponentExists.of_finite.{u}
+ added Group.exponent_dvd_nat_card.{u}
+ added AddMonoid.exponent_pos.{u}
+ added Monoid.exponent_dvd.{u}
+ added Monoid.orderOf_le_exponent.{u}
+ added Monoid.exponent_dvd_of_forall_orderOf_dvd.{u}
+ added Commute.of_orderOf_dvd_two.{u}
+ added AddMonoid.ExponentExists.exponent_ne_zero.{u}
+ added Group.exponent_dvd_card.{u}
+ added AddMonoid.exponent_ne_zero.{u}
+ added AddCommute.of_addOrderOf_dvd_two.{u}
+ added AddMonoid.ExponentExists.addOrderOf_pos.{u}
+ added addCommMonoidOfExponentTwo.{u}
+ added AddMonoid.exponent_dvd_iff_forall_nsmul_eq_zero.{u}
+ added Monoid.ExponentExists.exponent_pos.{u}
+ added AddMonoid.exponent_dvd.{u}
+ added Monoid.lcm_orderOf_eq_exponent.{u}
+ added Monoid.exists_orderOf_eq_exponent.{u}
+ added Monoid.exponent_ne_zero.{u}
! type changed for mul_not_mem_of_exponent_two
! type changed for mul_comm_of_exponent_two
! type changed for add_not_mem_of_addOrderOf_eq_two
! type changed for mul_not_mem_of_orderOf_eq_two
! type changed for inv_eq_self_of_exponent_two
! type changed for instCommGroupOfExponentTwo
! type changed for instAddCommGroupOfExponentTwo
! type changed for inv_eq_self_of_orderOf_eq_two
! type changed for add_comm_of_exponent_two
! type changed for neg_eq_self_of_addOrderOf_eq_two
! type changed for neg_eq_self_of_exponent_two
! type changed for orderOf_eq_two_iff
! type changed for add_not_mem_of_exponent_two
! type changed for addOrderOf_eq_two_iff
! type changed for AddMonoid.exponent_dvd_of_forall_nsmul_eq_zero
! type changed for Monoid.exponent_dvd_of_forall_pow_eq_one
+ attribute protected added to Monoid.ExponentExists.exponent_pos
+ attribute protected added to AddMonoid.ExponentExists.exponent_ne_zero
+ attribute reducible added to addCommMonoidOfExponentTwo
+ attribute reducible added to commMonoidOfExponentTwo
+ attribute protected added to AddMonoid.ExponentExists.exponent_pos
+ attribute protected added to Monoid.ExponentExists.exponent_ne_zero
! moved mul_not_mem_of_exponent_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved addOrderOf_eq_two_iff from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved add_not_mem_of_addOrderOf_eq_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved inv_eq_self_of_orderOf_eq_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved inv_eq_self_of_orderOf_eq_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved add_comm_of_exponent_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved add_comm_of_exponent_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved mul_comm_of_exponent_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved neg_eq_self_of_addOrderOf_eq_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved neg_eq_self_of_addOrderOf_eq_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved mul_not_mem_of_orderOf_eq_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved neg_eq_self_of_exponent_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved neg_eq_self_of_exponent_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved mul_not_mem_of_orderOf_eq_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved instCommGroupOfExponentTwo from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved instCommGroupOfExponentTwo from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved add_not_mem_of_exponent_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved add_not_mem_of_exponent_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved mul_comm_of_exponent_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved addOrderOf_eq_two_iff from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved inv_eq_self_of_exponent_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved orderOf_eq_two_iff from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved orderOf_eq_two_iff from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved inv_eq_self_of_exponent_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved add_not_mem_of_addOrderOf_eq_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved mul_not_mem_of_exponent_two from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved instAddCommGroupOfExponentTwo from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent
! moved instAddCommGroupOfExponentTwo from Mathlib.GroupTheory.SpecificGroups.KleinFour to Mathlib.GroupTheory.Exponent

[YaelDillies]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style