GroupTheory.Commutator no Ring

Mathlib/GroupTheory/Commutator/Basic.lean

@@ -3,9 +3,8 @@ Copyright (c) 2021 Jordan Brown, Thomas Browning, Patrick Lutz. All rights reser
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jordan Brown, Thomas Browning, Patrick Lutz
 -/
+import Mathlib.Algebra.Group.Commutator
 import Mathlib.GroupTheory.Subgroup.Centralizer
-import Mathlib.Tactic.Group
-import Mathlib.Order.ConditionallyCompleteLattice.Basic
 
 /-!
 # Commutators of Subgroups
@@ -20,7 +19,7 @@ is the subgroup of `G` generated by the commutators `h₁ * h₂ * h₁⁻¹ * h
 * `⁅H₁, H₂⁆` : the commutator of the subgroups `H₁` and `H₂`.
 -/
 
-assert_not_exists Cardinal Multiset
+assert_not_exists Cardinal Multiset Ring
 
 variable {G G' F : Type*} [Group G] [Group G'] [FunLike F G G'] [MonoidHomClass F G G']
 variable (f : F) {g₁ g₂ g₃ g : G}
@@ -93,9 +92,9 @@ theorem commutator_commutator_eq_bot_of_rotate (h1 : ⁅⁅H₂, H₃⁆, H₁
     mem_centralizer_iff_commutator_eq_one, ← commutatorElement_def] at h1 h2 ⊢
   intro x hx y hy z hz
   trans x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
-  · group
+  · simp [commutatorElement_def, mul_assoc]
   · rw [h1 _ (H₂.inv_mem hy) _ hz _ (H₁.inv_mem hx), h2 _ (H₃.inv_mem hz) _ (H₁.inv_mem hx) _ hy]
-    group
+    simp [commutatorElement_def, mul_assoc]
 
 variable (H₁ H₂)
 

Mathlib/GroupTheory/Commutator/Lemmas.lean

@@ -6,7 +6,9 @@ Authors: Jordan Brown, Thomas Browning, Patrick Lutz
 import Mathlib.Algebra.Group.Subgroup.Finite
 import Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
 import Mathlib.GroupTheory.Commutator.Basic
+import Mathlib.GroupTheory.Finiteness
 import Mathlib.GroupTheory.GroupAction.Quotient
+import Mathlib.GroupTheory.Index
 
 /-!
 # Extra lemmas about commutators
@@ -65,4 +67,16 @@ theorem quotientCenterEmbedding_apply {S : Set G} (hS : closure S = ⊤) (g : G)
     quotientCenterEmbedding hS g s = ⟨⁅g, s⁆, g, s, rfl⟩ :=
   rfl
 
+variable (G)
+
+instance finiteIndex_center [Finite (commutatorSet G)] [Group.FG G] : FiniteIndex (center G) := by
+  obtain ⟨S, -, hS⟩ := Group.rank_spec G
+  exact ⟨mt (Finite.card_eq_zero_of_embedding (quotientCenterEmbedding hS)) Finite.card_pos.ne'⟩
+
+lemma index_center_le_pow [Finite (commutatorSet G)] [Group.FG G] :
+    (center G).index ≤ Nat.card (commutatorSet G) ^ Group.rank G := by
+  obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
+  rw [← hS1, ← Fintype.card_coe, ← Nat.card_eq_fintype_card, ← Finset.coe_sort_coe, ← Nat.card_fun]
+  exact Finite.card_le_of_embedding (quotientCenterEmbedding hS2)
+
 end Subgroup

Mathlib/GroupTheory/Index.lean

@@ -5,10 +5,9 @@ Authors: Thomas Browning
 -/
 import Mathlib.Algebra.BigOperators.GroupWithZero.Finset
 import Mathlib.Data.Finite.Card
+import Mathlib.Data.Finite.Prod
 import Mathlib.Data.Set.Card
-import Mathlib.GroupTheory.Commutator.Lemmas
 import Mathlib.GroupTheory.Coset.Card
-import Mathlib.GroupTheory.Finiteness
 import Mathlib.GroupTheory.GroupAction.Quotient
 import Mathlib.GroupTheory.QuotientGroup.Basic
 
@@ -36,6 +35,7 @@ Several theorems proved in this file are known as Lagrange's theorem.
 - `MulAction.index_stabilizer`: the index of the stabilizer is the cardinality of the orbit
 -/
 
+assert_not_exists Field
 
 namespace Subgroup
 
@@ -598,18 +598,6 @@ instance finiteIndex_normalCore [H.FiniteIndex] : H.normalCore.FiniteIndex := by
   rw [normalCore_eq_ker]
   infer_instance
 
-variable (G)
-
-instance finiteIndex_center [Finite (commutatorSet G)] [Group.FG G] : FiniteIndex (center G) := by
-  obtain ⟨S, -, hS⟩ := Group.rank_spec G
-  exact ⟨mt (Finite.card_eq_zero_of_embedding (quotientCenterEmbedding hS)) Finite.card_pos.ne'⟩
-
-theorem index_center_le_pow [Finite (commutatorSet G)] [Group.FG G] :
-    (center G).index ≤ Nat.card (commutatorSet G) ^ Group.rank G := by
-  obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
-  rw [← hS1, ← Fintype.card_coe, ← Nat.card_eq_fintype_card, ← Finset.coe_sort_coe, ← Nat.card_fun]
-  exact Finite.card_le_of_embedding (quotientCenterEmbedding hS2)
-
 end FiniteIndex
 
 end Subgroup