subgroup_mul_singleton

Mathlib.Algebra.Group.Subgroup.Pointwise

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

← MathLib Explorer

English

If h ∈ H, then H multiplied by the singleton {h} equals H.

Русский

Если h ∈ H, то H умноженное на одиночку {h} равно H.

LaTeX

$$$ H \cdot \{h\} = H \quad \text{if } h \in H $$$

Lean4

theorem subgroup_mul_singleton {H : Subgroup G} {h : G} (hh : h ∈ H) : (H : Set G) * { h } = H := by
  simp [preimage, mul_mem_cancel_right (inv_mem hh)]

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

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

Разделы

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

Аффилиация

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