Theorems · Definition · group theory

AddSubgroup.goursatFst

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