commensurator'_mem_iff

Mathlib.GroupTheory.Commensurable

URI: https://scilib.ai/kg/mathlib#Subgroup.Commensurable.commensurator'_mem_iff

English

The membership of g in commensurator' H is equivalent to Commensurable (g • H) H.

Русский

Членство g в commensurator' H эквивалентно комменсируемости g • H и H.

LaTeX

$$g ∈ commensurator' H ↔ Commensurable (g • H) H$$

Lean4

@[simp]
theorem commensurator'_mem_iff (H : Subgroup G) (g : ConjAct G) : g ∈ commensurator' H ↔ Commensurable (g • H) H :=
  Iff.rfl

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

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

Разделы

Аффилиация

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