variables

Author: tb65536

Mathlib/GroupTheory/Commensurable.lean

@@ -39,7 +39,7 @@ additively.
 
 open scoped Pointwise
 
-variable {G G' : Type*} [Group G] [Group G']
+variable {G G' : Type*} [Group G] [Group G'] {H K L : Subgroup G}
 
 /-- Equivalence of `K / (H ⊓ K)` with `gKg⁻¹/ (gHg⁻¹ ⊓ gKg⁻¹)` -/
 @[deprecated "This technical lemma is no longer necessary for the proof of `commensurable_conj`."
@@ -64,13 +64,13 @@ namespace Subgroup.Commensurable
 protected theorem refl (H : Subgroup G) : Commensurable H H := by simp [Commensurable]
 
 @[to_additive]
-theorem comm {H K : Subgroup G} : Commensurable H K ↔ Commensurable K H := and_comm
+theorem comm : Commensurable H K ↔ Commensurable K H := and_comm
 
 @[to_additive (attr := symm)]
-theorem symm {H K : Subgroup G} : Commensurable H K → Commensurable K H := And.symm
+theorem symm : Commensurable H K → Commensurable K H := And.symm
 
 @[to_additive (attr := trans)]
-theorem trans {H K L : Subgroup G} (hhk : Commensurable H K) (hkl : Commensurable K L) :
+theorem trans (hhk : Commensurable H K) (hkl : Commensurable K L) :
     Commensurable H L :=
   ⟨hhk.1.trans hkl.1, hkl.2.trans hhk.2⟩
 
@@ -79,62 +79,58 @@ theorem equivalence : Equivalence (@Commensurable G _) :=
   ⟨Commensurable.refl, fun h => Commensurable.symm h, fun h₁ h₂ => Commensurable.trans h₁ h₂⟩
 
 @[to_additive (attr := simp)]
-theorem top_left_iff {H : Subgroup G} : Commensurable ⊤ H ↔ H.FiniteIndex := by
+theorem top_left_iff : Commensurable ⊤ H ↔ H.FiniteIndex := by
   simp [Commensurable, isFiniteRelIndex_iff_relIndex_ne_zero, finiteIndex_iff]
 
 @[to_additive (attr := simp)]
-theorem top_right_iff {H : Subgroup G} : Commensurable H ⊤ ↔ H.FiniteIndex := by
+theorem top_right_iff : Commensurable H ⊤ ↔ H.FiniteIndex := by
   simp [Commensurable, isFiniteRelIndex_iff_relIndex_ne_zero, finiteIndex_iff]
 
 @[to_additive (attr := simp)]
-theorem bot_left_iff {H : Subgroup G} : Commensurable ⊥ H ↔ Finite H := by
+theorem bot_left_iff : Commensurable ⊥ H ↔ Finite H := by
   simp [Commensurable, isFiniteRelIndex_iff_relIndex_ne_zero, Nat.card_ne_zero, One.instNonempty]
 
 @[to_additive (attr := simp)]
-theorem bot_right_iff {H : Subgroup G} : Commensurable H ⊥ ↔ Finite H := by
+theorem bot_right_iff : Commensurable H ⊥ ↔ Finite H := by
   simp [Commensurable, isFiniteRelIndex_iff_relIndex_ne_zero, Nat.card_ne_zero, One.instNonempty]
 
-theorem inf_left {H K L : Subgroup G} (hHL : Commensurable H L) (hKL : Commensurable K L) :
+theorem inf_left (hHL : Commensurable H L) (hKL : Commensurable K L) :
     Commensurable (H ⊓ K) L :=
   ⟨hHL.1.inf hKL.1, have := hHL.2; isFiniteRelIndex_of_le_right L inf_le_left⟩
 
-theorem inf_right {H K L : Subgroup G} (hHK : Commensurable H K) (hHL : Commensurable H L) :
+theorem inf_right (hHK : Commensurable H K) (hHL : Commensurable H L) :
     Commensurable H (K ⊓ L) :=
   ⟨have := hHL.1; isFiniteRelIndex_of_le_right H inf_le_right, hHK.2.inf hHL.2⟩
 
-protected theorem map {H K : Subgroup G} (f : G →* G') (h : H.Commensurable K) :
+protected theorem map (f : G →* G') (h : H.Commensurable K) :
     Commensurable (H.map f) (K.map f) :=
   h.imp (.map f) (.map f)
 
-protected theorem comap {H K : Subgroup G} (f : G' →* G) (h : H.Commensurable K) :
+protected theorem comap (f : G' →* G) (h : H.Commensurable K) :
     Commensurable (H.comap f) (K.comap f) :=
   h.imp (.comap f) (.comap f)
 
-theorem map_injective_iff {H K : Subgroup G} {f : G →* G'} (hf : Function.Injective f) :
+theorem map_injective_iff {f : G →* G'} (hf : Function.Injective f) :
     Commensurable (H.map f) (K.map f) ↔ Commensurable H K :=
   ⟨fun h ↦ by simpa [comap_map_eq_self_of_injective hf] using h.comap f, .map f⟩
 
-theorem comap_surjective_iff {H K : Subgroup G}
-    {f : G' →* G} (hf : Function.Surjective f) :
+theorem comap_surjective_iff {f : G' →* G} (hf : Function.Surjective f) :
     Commensurable (H.comap f) (K.comap f) ↔ Commensurable H K :=
   ⟨fun h ↦ by simpa [map_comap_eq_self_of_surjective hf] using h.map f, .comap f⟩
 
-protected theorem smul {H K : Subgroup G}
-    {Φ : Type*} [Group Φ] [MulDistribMulAction Φ G] (φ : Φ) (h : H.Commensurable K) :
-    Commensurable (φ • H) (φ • K) :=
+protected theorem smul {Φ : Type*} [Group Φ] [MulDistribMulAction Φ G] (φ : Φ)
+    (h : H.Commensurable K) : Commensurable (φ • H) (φ • K) :=
   h.map _
 
 @[deprecated (since := "2026-06-25")] alias conj := Subgroup.Commensurable.smul
 
-theorem smul_iff {H K : Subgroup G}
-    {Φ : Type*} [Group Φ] [MulDistribMulAction Φ G] {φ : Φ} :
+theorem smul_iff {Φ : Type*} [Group Φ] [MulDistribMulAction Φ G] {φ : Φ} :
     Commensurable (φ • H) (φ • K) ↔ Commensurable H K :=
   ⟨fun h ↦ by simpa using h.smul φ⁻¹, .smul φ⟩
 
 @[deprecated (since := "2026-06-25")] alias commensurable_conj := Subgroup.Commensurable.smul_iff
 
-theorem inv_smul_iff {H K : Subgroup G}
-    {Φ : Type*} [Group Φ] [MulDistribMulAction Φ G] {φ : Φ} :
+theorem inv_smul_iff {Φ : Type*} [Group Φ] [MulDistribMulAction Φ G] {φ : Φ} :
     Commensurable (φ⁻¹ • H) K ↔ Commensurable H (φ • K) := by
   simpa using smul_iff (H := H) (K := φ • K) (φ := φ⁻¹)
 
@@ -164,7 +160,7 @@ theorem commensurator'_mem_iff (H : Subgroup G) (g : ConjAct G) :
   rw [commensurator', map_equiv_eq_comap_symm']
   rfl
 
-theorem eq {H K : Subgroup G} (hk : Commensurable H K) : commensurator H = commensurator K :=
+theorem eq (hk : Commensurable H K) : commensurator H = commensurator K :=
   Subgroup.ext fun x =>
     let hx := hk.smul (MulAut.conj x)
     ⟨fun h => hx.symm.trans (h.trans hk), fun h => hx.trans (h.trans hk.symm)⟩