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

Mathlib/Algebra/Group/Commute/Defs.lean

@@ -50,6 +50,9 @@ section Mul
 
 variable {S : Type*} [Mul S]
 
+@[to_additive]
+theorem _root_.commute_def {a b : S} : Commute a b ↔ a * b = b * a := .rfl
+
 /-- Equality behind `Commute a b`; useful for rewriting. -/
 @[to_additive "Equality behind `AddCommute a b`; useful for rewriting."]
 protected theorem eq {a b : S} (h : Commute a b) : a * b = b * a :=

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

@@ -616,7 +616,7 @@ theorem IsCyclic.exponent_eq_card [Group α] [IsCyclic α] [Fintype α] :
     exponent α = Fintype.card α := by
   obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
   apply Nat.dvd_antisymm
-  · rw [← lcm_order_eq_exponent, Finset.lcm_dvd_iff]
+  · rw [← lcm_orderOf_eq_exponent, Finset.lcm_dvd_iff]
     exact fun b _ => orderOf_dvd_card
   rw [← orderOf_eq_card_of_forall_mem_zpowers hg]
   exact order_dvd_exponent _

Mathlib/GroupTheory/SpecificGroups/Dihedral.lean

@@ -195,7 +195,7 @@ theorem exponent : Monoid.exponent (DihedralGroup n) = lcm n 2 := by
   rcases eq_zero_or_neZero n with (rfl | hn)
   · exact Monoid.exponent_eq_zero_of_order_zero orderOf_r_one
   apply Nat.dvd_antisymm
-  · apply Monoid.exponent_dvd_of_forall_pow_eq_one
+  · rw [Monoid.exponent_dvd_iff_forall_pow_eq_one]
     rintro (m | m)
     · rw [← orderOf_dvd_iff_pow_eq_one, orderOf_r]
       refine' Nat.dvd_trans ⟨gcd n m.val, _⟩ (dvd_lcm_left n 2)

Mathlib/GroupTheory/SpecificGroups/KleinFour.lean

@@ -40,55 +40,6 @@ produces the third one.
 non-cyclic abelian group
 -/
 
-/-! # Properties of groups with exponent two -/
-
-section ExponentTwo
-
-variable {G : Type*} [Group G]
-
-/-- In a group of exponent two, every element is its own inverse. -/
-@[to_additive]
-lemma inv_eq_self_of_exponent_two (hG : Monoid.exponent G = 2) (x : G) :
-    x⁻¹ = x :=
-  inv_eq_of_mul_eq_one_left <| pow_two (a := x) ▸ hG ▸ Monoid.pow_exponent_eq_one x
-
-/-- If an element in a group has order two, then it is its own inverse. -/
-@[to_additive]
-lemma inv_eq_self_of_orderOf_eq_two {x : G} (hx : orderOf x = 2) :
-    x⁻¹ = x :=
-  inv_eq_of_mul_eq_one_left <| pow_two (a := x) ▸ hx ▸ pow_orderOf_eq_one x
-
-@[to_additive]
-lemma orderOf_eq_two_iff (hG : Monoid.exponent G = 2) {x : G} :
-    orderOf x = 2 ↔ x ≠ 1 :=
-  ⟨by rintro hx rfl; norm_num at hx, orderOf_eq_prime (hG ▸ Monoid.pow_exponent_eq_one x)⟩
-
-/-- In a group of exponent two, all elements commute. -/
-@[to_additive]
-lemma mul_comm_of_exponent_two (hG : Monoid.exponent G = 2) (x y : G) :
-    x * y = y * x := by
-  simpa only [inv_eq_self_of_exponent_two hG] using mul_inv_rev x y
-
-/-- Any group of exponent two is abelian. -/
-@[to_additive (attr := reducible) "Any additive group of exponent two is abelian."]
-def instCommGroupOfExponentTwo (hG : Monoid.exponent G = 2) : CommGroup G where
-  mul_comm := mul_comm_of_exponent_two hG
-
-@[to_additive]
-lemma mul_not_mem_of_orderOf_eq_two {G : Type*} [Group G] {x y : G} (hx : orderOf x = 2)
-    (hy : orderOf y = 2) (hxy : x ≠ y) : x * y ∉ ({x, y, 1} : Set G) := by
-  simp only [Set.mem_singleton_iff, Set.mem_insert_iff, mul_right_eq_self, mul_left_eq_self,
-    mul_eq_one_iff_eq_inv, inv_eq_self_of_orderOf_eq_two hy, not_or]
-  aesop
-
-@[to_additive]
-lemma mul_not_mem_of_exponent_two {G : Type*} [Group G] (h : Monoid.exponent G = 2) {x y : G}
-    (hx : x ≠ 1) (hy : y ≠ 1) (hxy : x ≠ y) : x * y ∉ ({x, y, 1} : Set G) :=
-  mul_not_mem_of_orderOf_eq_two (orderOf_eq_prime (h ▸ Monoid.pow_exponent_eq_one x) hx)
-    (orderOf_eq_prime (h ▸ Monoid.pow_exponent_eq_one y) hy) hxy
-
-end ExponentTwo
-
 /-! # Klein four-groups as a mixin class -/
 
 /-- An (additive) Klein four-group is an (additive) group of cardinality four and exponent two. -/

Mathlib/GroupTheory/SpecificGroups/Quaternion.lean

@@ -268,7 +268,7 @@ theorem exponent : Monoid.exponent (QuaternionGroup n) = 2 * lcm n 2 := by
     simp only [lcm_zero_left, mul_zero]
     exact Monoid.exponent_eq_zero_of_order_zero orderOf_a_one
   apply Nat.dvd_antisymm
-  · apply Monoid.exponent_dvd_of_forall_pow_eq_one
+  · rw [Monoid.exponent_dvd_iff_forall_pow_eq_one]
     rintro (m | m)
     · rw [← orderOf_dvd_iff_pow_eq_one, orderOf_a]
       refine' Nat.dvd_trans ⟨gcd (2 * n) m.val, _⟩ (dvd_lcm_left (2 * n) 4)

Mathlib/GroupTheory/Torsion.lean

@@ -138,15 +138,15 @@ theorem ExponentExists.isTorsion (h : ExponentExists G) : IsTorsion G := fun g =
       "The group exponent exists for any bounded additive torsion group."]
 theorem IsTorsion.exponentExists (tG : IsTorsion G)
     (bounded : (Set.range fun g : G => orderOf g).Finite) : ExponentExists G :=
-  exponentExists_iff_ne_zero.mpr <|
+  exponent_ne_zero.mp <|
     (exponent_ne_zero_iff_range_orderOf_finite fun g => (tG g).orderOf_pos).mpr bounded
 #align is_torsion.exponent_exists IsTorsion.exponentExists
 #align is_add_torsion.exponent_exists IsAddTorsion.exponentExists
 
 /-- Finite groups are torsion groups. -/
 @[to_additive is_add_torsion_of_finite "Finite additive groups are additive torsion groups."]
 theorem isTorsion_of_finite [Finite G] : IsTorsion G :=
-  ExponentExists.isTorsion <| exponentExists_iff_ne_zero.mpr exponent_ne_zero_of_finite
+  ExponentExists.isTorsion <| exponent_ne_zero.mp exponent_ne_zero_of_finite
 #align is_torsion_of_finite isTorsion_of_finite
 #align is_add_torsion_of_finite is_add_torsion_of_finite