prod — Mathlib

English

Two elements x=(x1,x2) and y=(y1,y2) in M × N commute if and only if x1 commutes y1 and x2 commutes y2.

Русский

Два элемента x=(x1,x2) и y=(y1,y2) в M × N коммутируют тогда и только тогда, когда x1 коммутирует y1 и x2 коммутирует y2.

LaTeX

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

Lean4

@[to_additive AddCommute.prod]
theorem prod {x y : M × N} (hm : Commute x.1 y.1) (hn : Commute x.2 y.2) : Commute x y :=
  SemiconjBy.prod hm hn

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