Theorems · Definition · group theory

AddSubgroup.goursatSnd

{G : Type u_1} → {H : Type u_2} → [inst : AddGroup G] → [inst_1 : AddGroup H] → AddSubgroup (G × H) → AddSubgroup H

For I a subgroup of G × H, I.goursatSnd is the kernel of the projection map I → G, considered as a subgroup of H. This is the second subgroup appearing in Goursat's lemma. See AddSubgroup.goursat.

Defined in

Mathlib.GroupTheory.Goursat

Cited by

8 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

AddGroupAddGroup