feat(Algebra/Group/Subgroup/Ker): kernel of a homomorphism composed with an isomorphism (leanprover-community#34580)

feat(Algebra/Group/Subgroup/Ker):  kernel of a homomorphism composed with an isomorphism

The kernel of a homomorphism composed with an isomorphism is equal to the kernel of
the homomorphism mapped by the inverse isomorphism.

This is a dependency of a larger PR to formalize finitely presented groups leanprover-community#34236.

Author: homeowmorphism

Mathlib/Algebra/Group/Subgroup/Ker.lean

@@ -259,6 +259,13 @@ theorem comap_ker {P : Type*} [MulOneClass P] (g : N →* P) (f : G →* N) :
     g.ker.comap f = (g.comp f).ker :=
   rfl
 
+/-- The kernel of a homomorphism composed with an isomorphism is equal to the kernel of
+the homomorphism mapped by the inverse isomorphism. -/
+@[to_additive (attr := simp)]
+lemma ker_comp_mulEquiv {P : Type*} [MulOneClass P]
+  (g : N →* P) (iso : G ≃* N) : (g.comp iso).ker = map (iso.symm : N →* G) g.ker := by
+  rw [← comap_ker, comap_equiv_eq_map_symm]
+
 @[to_additive (attr := simp)]
 theorem comap_bot (f : G →* N) : (⊥ : Subgroup N).comap f = f.ker :=
   rfl