div_mem_comm_iff

Mathlib.Algebra.Group.Subgroup.Basic

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

English

An alias form of the same div_mem_comm_iff: a b^{-1} ∈ H ⇔ b a^{-1} ∈ H.

Русский

Алиас той же формулы: a b^{-1} ∈ H ↔ b a^{-1} ∈ H.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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