subgroup_quotientGroupCon

Mathlib.GroupTheory.QuotientGroup.Defs

URI: https://scilib.ai/kg/mathlib#Con.subgroup_quotientGroupCon

← MathLib Explorer

English

For a subgroup H with H.normal, QuotientGroup.con H.subgroup = H.

Русский

Для подгруппы H, нормальной, QuotientGroup.con H.subgroup = H.

LaTeX

$$QuotientGroup.con H.subgroup = H$$

Lean4

@[to_additive (attr := simp)]
theorem _root_.Con.subgroup_quotientGroupCon (H : Subgroup G) [H.Normal] : (QuotientGroup.con H).subgroup = H :=
  by
  ext
  simp [QuotientGroup.con, leftRel_apply]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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