neg_one_left

Mathlib.Algebra.Ring.Commute

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

English

For a ring R with MulOneClass and HasDistribNeg, -1 commutes with a on the left.

Русский

Для кольца R с MulOneClass и HasDistribNeg, -1 коммутирует с a слева.

LaTeX

$$$\\text{Commute } (-1) a$$$

Lean4

theorem neg_one_left (a : R) : Commute (-1) a :=
  SemiconjBy.neg_one_left a

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

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

Разделы

Аффилиация

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