Theorems · Definition · group theory

Subgroup.goursatFst

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

For I a subgroup of G × H, I.goursatFst is the kernel of the projection map I → H, considered as a subgroup of G. This is the first 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