fst_comp_prodAssoc — Mathlib

English

The first projection after applying prodAssoc equals the composed first projection in the nested setup; i.e., a refined equality of two linear maps.

Русский

Первая проекция после применения prodAssoc равна композиции проекции fst в вложенной конфигурации.

LaTeX

$$$\mathrm{fst} R M_1 (M_2) \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 fst_comp_prodAssoc :
    (LinearMap.fst R M₁ (M₂ × M₃)).comp (prodAssoc R M₁ M₂ M₃).toLinearMap =
      (LinearMap.fst R M₁ M₂).comp (LinearMap.fst R (M₁ × M₂) M₃) :=
  by ext <;> simp

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