feat(group_theory/subgroup/basic): If H is commutative, then `H ≤ H…

….centralizer` (#16718) If `H` is commutative, then `H ≤ H.centralizer`.
leanprover-community · Oct 1, 2022 · d638c7f · d638c7f
1 parent 567220c
commit d638c7f
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
@@ -1859,6 +1859,12 @@ end⟩⟩
   (H.subgroup_of K).is_commutative :=
 H.comap_injective_is_commutative subtype.coe_injective
 
+@[to_additive] lemma le_centralizer_iff_is_commutative : K ≤ K.centralizer ↔ K.is_commutative :=
+⟨λ h, ⟨⟨λ x y, subtype.ext (h y.2 x x.2)⟩⟩, λ h x hx y hy, congr_arg coe (h.1.1 ⟨y, hy⟩ ⟨x, hx⟩)⟩
+
+@[to_additive] lemma le_centralizer [h : H.is_commutative] : H ≤ H.centralizer :=
+le_centralizer_iff_is_commutative.mpr h
+
 end subgroup
 
 namespace group