snd_comp_prodComm — Mathlib

English

The first projection after reassociating a triple product equals the successive first projections; i.e., the two natural ways of extracting the first component agree.

Русский

Первая проекция после перестановной ассоциации тройного произведения совпадает с последовательными проекциями; оба способа извлечения первой компоненты совпадают.

LaTeX

$$$\mathrm{fst}\ R\ M_1 (M_2 \times M_3) \circ \mathrm{prodAssoc}\ R\ M_1 M_2 M_3 = \mathrm{fst}\ R\ M_1 M_2 \circ \mathrm{fst}\ R (M_1 \times M_2) M_3$$$

Lean4

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

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