coe_prodMap — Mathlib

English

The underlying map of the product map equals the product of the underlying linear maps.

Русский

Функционально отображение произведения равно произведению соответствующих линейных отображений.

LaTeX

$$$\\uparrow(f_1.prodMap f_2) = (f_1 : M_1 \\to M_2) .prodMap (f_2 : M_3 \\to M_4)$$$

Lean4

@[simp, norm_cast]
theorem coe_prodMap (f₁ : M₁ →L[R] M₂) (f₂ : M₃ →L[R] M₄) :
    ↑(f₁.prodMap f₂) = (f₁ : M₁ →ₗ[R] M₂).prodMap (f₂ : M₃ →ₗ[R] M₄) :=
  rfl

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