English
For a subgroup I of G × H, the first Gerg kernel is the subset of G consisting of all g with (g, e_H) ∈ I.
Русский
Для подгруппы I подмножество G, состоящее из всех элементов g, таких что (g, e_H) ∈ I.
LaTeX
$$$$I.goursatFst = \\{ g \\in G \\mid (g, e_H) \\in I \\}.$$$$
Lean4
/-- 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`. -/
@[to_additive /-- 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`. -/
]
def goursatFst : Subgroup G :=
((MonoidHom.snd G H).comp I.subtype).ker.map ((MonoidHom.fst G H).comp I.subtype)
