commute_iff

Mathlib.Algebra.Group.Prod

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

English

Two elements x,y in M × N commute iff their coordinates commute componentwise.

Русский

Два элемента x,y в M × N commute тогда и только тогда, когда их координаты commute по частям.

LaTeX

$$$Commute(x,y) \iff (Commute(x_1,y_1) \land Commute(x_2,y_2))$$$

Lean4

@[to_additive]
theorem commute_iff {x y : M × N} : Commute x y ↔ Commute x.1 y.1 ∧ Commute x.2 y.2 :=
  semiconjBy_iff

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

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

Разделы

Аффилиация

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