Theorems · Definition · group theory

Subgroup.goursatSnd

{G : Type u_1} → {H : Type u_2} → [inst : Group G] → [inst_1 : Group H] → Subgroup (G × H) → Subgroup 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 Subgroup.goursat.

Defined in

Mathlib.GroupTheory.Goursat

Cited by

6 results in Mathlib

Foundations

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

Assumes

GroupGroup