tprod — Mathlib

English

If a1 and a2 commute componentwise, then their PiTensorProduct tensor expressions commute: tprod R a1 and tprod R a2 commute.

Русский

Если группы a1 и a2 коммутируют компонентно, то их тензорные произведения по PiTensorProduct также коммутируют.

LaTeX

$$$Commute\\ (tprod\\ R\\ a_1)\\ (tprod\\ R\\ a_2)$$$

Lean4

nonrec theorem _root_.Commute.tprod {a₁ a₂ : Π i, A i} (ha : Commute a₁ a₂) : Commute (tprod R a₁) (tprod R a₂) :=
  ha.tprod

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