unop

Mathlib.Algebra.Group.Opposite

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

English

If x and y commute in αᵐᵒᵖ, then unop x and unop y commute in α.

Русский

Если x и y коммутируют в αᵐᵒᵖ, то unop x и unop y коммутируют в α.

LaTeX

$$$\\text{Commute}(\\operatorname{unop} x, \\operatorname{unop} y)$$$

Lean4

@[to_additive]
nonrec theorem _root_.Commute.unop [Mul α] {x y : αᵐᵒᵖ} (h : Commute x y) : Commute (unop x) (unop y) :=
  h.unop

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

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

Разделы

Аффилиация

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