symm_iff

Mathlib.Algebra.Group.Commute.Defs

URI: https://scilib.ai/kg/mathlib#Commute.symm_iff

English

Commute is symmetric: Commute a b iff Commute b a.

Русский

Коммутирование симметрично: Commute a b ⇔ Commute b a.

LaTeX

$$$\\forall S [Mul S],\\ {a,b:\\ S},\\ Commute a b \\leftrightarrow Commute b a$$$

Lean4

@[to_additive]
protected theorem symm_iff {a b : S} : Commute a b ↔ Commute b a :=
  ⟨Commute.symm, Commute.symm⟩

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

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

Разделы

Аффилиация

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