snd_comp_prodAssoc — Mathlib

English

The second projection after prodAssoc factors as the product of the first projection and the identity on the third component.

Русский

Вторая проекция после prodAssoc разбивается как произведение проекции fst на M2 и единицы на M3.

LaTeX

$$$\mathrm{snd} R M_1 (M_2 \times M_3) \circ \mathrm{prodAssoc} R M_1 M_2 M_3 = \mathrm{prodMap}(\mathrm{fst} R M_1 M_2)\, (\mathrm{id}_{M_3})$$$

Lean4

theorem snd_comp_prodAssoc :
    (LinearMap.snd R M₁ (M₂ × M₃)).comp (prodAssoc R M₁ M₂ M₃).toLinearMap =
      (LinearMap.snd R M₁ M₂).prodMap (LinearMap.id : M₃ →ₗ[R] M₃) :=
  by ext <;> simp

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