instNormalSubgroup

Mathlib.GroupTheory.QuotientGroup.Defs

URI: https://scilib.ai/kg/mathlib#QuotientGroup.instNormalSubgroup

English

The quotient of a group by a congruence c corresponds to the subgroup c.subgroup.

Русский

Квазиобраз фактор-группы по конгруэнции c соответствует подгруппе c.subgroup.

LaTeX

$$QuotientGroup.con c.subgroup = c$$

Lean4

@[to_additive]
instance (c : Con G) : c.subgroup.Normal :=
  ⟨fun x hx g ↦ by simpa using (c.mul (c.mul (c.refl g) hx) (c.refl g⁻¹))⟩

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

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

Разделы

Аффилиация

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