neg_left_iff

Mathlib.Algebra.Ring.Commute

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

English

Commute(-a) b iff Commute a b.

Русский

Commute(-a) b эквивалентно Commute a b.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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