feat(FinitelyPresentedGroup): quotient of a finitely group by a subgroup which is finitely generated under normal closure is finitely presented (leanprover-community#40845)

Add theorem that the quotient of a finitely presented group by a subgroup whose normal closure is finitely generated is finitely presented. leanprover-community#38930

Also add docstring and `@[to_additive]` annotation to `of_surjective`.

Co-authored-by: Hang Lu Su <hanglu.su@pm.me>

Author: laredo02

Mathlib/GroupTheory/FinitelyPresentedGroup.lean

@@ -103,6 +103,10 @@ theorem equiv (iso : G ≃* H) [h : IsFinitelyPresented G] : IsFinitelyPresented
   refine ⟨n, (iso : G →* H).comp φ, iso.surjective.comp hφsurj, ?_⟩
   rwa [φ.ker_mulEquiv_comp iso]
 
+/-- The image of a finitely presented group under a surjective homomorphism whose kernel is
+finitely generated as a normal subgroup is finitely presented. -/
+@[to_additive /-- The image of a finitely presented additive group under a surjective additive
+homomorphism whose kernel is finitely generated as a normal subgroup is finitely presented. -/]
 theorem of_surjective [hG : IsFinitelyPresented G] (f : G →* H)
     (hf_surj : Function.Surjective f) (hf_ker : f.ker.IsNormalClosureFG) :
     IsFinitelyPresented H := by
@@ -111,6 +115,15 @@ theorem of_surjective [hG : IsFinitelyPresented G] (f : G →* H)
   rw [← MonoidHom.comap_ker]
   exact hf_ker.comap hφ_surj hφ_ker
 
+/-- The quotient of a finitely presented group by a subgroup
+which is finitely generated as a normal subgroup is finitely presented. -/
+@[to_additive /-- The quotient of a finitely presented additive group by an additive subgroup
+which is finitely generated as a normal subgroup is finitely presented. -/]
+theorem quotient [hG : IsFinitelyPresented G] (N : Subgroup G) [N.Normal]
+    (hN : N.IsNormalClosureFG) : IsFinitelyPresented (G ⧸ N) :=
+  of_surjective (QuotientGroup.mk' N) (QuotientGroup.mk'_surjective N)
+    ((QuotientGroup.ker_mk' N).symm ▸ hN)
+
 open QuotientGroup in
 theorem exists_mulEquiv_presentedGroup [hg : IsFinitelyPresented G] :
     ∃ n : ℕ, ∃ s : Set (FreeGroup (Fin n)), Set.Finite s ∧ Nonempty (G ≃* PresentedGroup s) := by