commute_iff

Mathlib.Algebra.Group.Pi.Lemmas

URI: https://scilib.ai/kg/mathlib#Pi.commute_iff

English

Two pi-valued elements x and y commute if and only if their corresponding coordinates commute pointwise.

Русский

Две Pi-значения x и y commute тогда, когда их координаты коммутируют по точкам.

LaTeX

$$$\mathrm{Commute}(x,y) \iff \forall i, \mathrm{Commute}(x_i, y_i)$$$

Lean4

@[to_additive]
theorem commute_iff {x y : ∀ i, f i} : Commute x y ↔ ∀ i, Commute (x i) (y i) :=
  semiconjBy_iff

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

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

Разделы

Аффилиация

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