mem_goursatSnd

Mathlib.GroupTheory.Goursat

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

English

For any g in G, g ∈ I.goursatFst iff (g,1) ∈ I.

Русский

Для любого g в G выполняется g ∈ I.goursatFst тогда и только тогда, когда (g,1) ∈ I.

LaTeX

$$$$g \\in I.goursatFst \\;\\iff\\; (g,1) \\in I.$$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_goursatSnd {h : H} : h ∈ I.goursatSnd ↔ (1, h) ∈ I := by simp [goursatSnd]

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

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

Разделы

Аффилиация

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