isComplement'_comm

Mathlib.GroupTheory.Complement

URI: https://scilib.ai/kg/mathlib#Subgroup.isComplement'_comm

English

isComplement'_comm: IsComplement' H K ↔ IsComplement' K H.

Русский

isComplement'_comm: IsComplement' H K ↔ IsComplement' K H.

LaTeX

$$$ \text{isComplement'_comm } : IsComplement' H K \leftrightarrow IsComplement' K H. $$$

Lean4

@[to_additive]
theorem isComplement'_comm : IsComplement' H K ↔ IsComplement' K H :=
  ⟨IsComplement'.symm, IsComplement'.symm⟩

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

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

Разделы

Аффилиация

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