fst_comp_prodComm — Mathlib

English

The additive structure underlying the swap isomorphism aligns with the corresponding AddEquiv on products.

Русский

Аддитивная структура изоморфизма перестановки соответствует соответствующему AddEquiv на произведениях.

LaTeX

$$$(\mathrm{prodComm}\ R\ M\ N).toAddEquiv = \mathrm{AddEquiv.prodComm} M N$$$

Lean4

theorem fst_comp_prodComm : (LinearMap.fst R M₂ M).comp (prodComm R M M₂).toLinearMap = (LinearMap.snd R M M₂) := by
  ext <;> simp

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