commute_unop

Mathlib.Algebra.Group.Opposite

URI: https://scilib.ai/kg/mathlib#MulOpposite.commute_unop

← MathLib Explorer

English

Commute (unop x) (unop y) holds if and only if Commute x y holds.

Русский

Commute (unop x) (unop y) выполняется тогда, когда Commute x y выполняется.

LaTeX

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

Lean4

@[to_additive (attr := simp, nolint simpComm)]
theorem commute_unop [Mul α] {x y : αᵐᵒᵖ} : Commute (unop x) (unop y) ↔ Commute x y :=
  semiconjBy_unop

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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