mem_goursatFst

Mathlib.GroupTheory.Goursat

URI: https://scilib.ai/kg/mathlib#Subgroup.mem_goursatFst

English

If the projection of I to G is surjective, then I.goursatFst is a normal subgroup of G.

Русский

Если проекция I на G сюръективна, то I.goursatFst является нормальной подгруппой G.

LaTeX

$$$$\\text{If } hI_1\\text{ is surjective, then } I.goursatFst \\triangleleft G.$$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_goursatFst {g : G} : g ∈ I.goursatFst ↔ (g, 1) ∈ I := by simp [goursatFst]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru