Theorems · Theorem · group theory

AddGroup.IsFinitelyPresented.of_surjective

∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] [hG : AddGroup.IsFinitelyPresented G]
  (f : G →+ H), Function.Surjective ⇑f → f.ker.IsFinitelyNormallyGenerated → AddGroup.IsFinitelyPresented H

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.

Defined in

Mathlib.GroupTheory.FinitelyPresentedGroup

Cited by

1 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddGroupAddGroup.IsFinitelyPresented