div_mem_comm_iff

Mathlib.Algebra.Group.Subgroup.Basic

URI: https://scilib.ai/kg/mathlib#div_mem_comm_iff

English

For a subgroup H of G and elements a,b ∈ G, a b^{-1} ∈ H if and only if b a^{-1} ∈ H.

Русский

Для подгруппы H ⊆ G и элементов a,b ∈ G выполняется: a b^{-1} ∈ H тогда и только тогда, когда b a^{-1} ∈ H.

LaTeX

$$$a b^{-1} \in H \;\iff\; b a^{-1} \in H$$$

Lean4

@[to_additive]
theorem div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H :=
  inv_div b a ▸ inv_mem_iff

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

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

Разделы

Аффилиация

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