neg_right_iff

Mathlib.Algebra.Ring.Commute

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

English

Commute a with -b is equivalent to commuting a with b.

Русский

Коммутирование a с -b эквивалентно коммутированию a с b.

LaTeX

$$$\\text{Commute } a (-b) \\iff \\text{Commute } a b$$$

Lean4

@[simp]
theorem neg_right_iff : Commute a (-b) ↔ Commute a b :=
  SemiconjBy.neg_right_iff

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

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

Разделы

Аффилиация

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