singleton_mul_subgroup

Mathlib.Algebra.Group.Subgroup.Pointwise

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

← MathLib Explorer

English

Similarly, {h} multiplied by H equals H if h ∈ H.

Русский

Аналогично, {h} умноженное на H равно H при условии h ∈ H.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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