prodMapLinear — Mathlib

English

Another instance of the composition compatibility: (f2∘f1).prodMap (g2∘g1) equals f2.prodMap g2 composed with f1.prodMap g1.

Русский

Ещё один пример совместимости композиции: (f2∘f1).prodMap (g2∘g1) = (f2.prodMap g2) ∘ (f1.prodMap g1).

LaTeX

$$$ (f_2 \\circ f_1) \\text{ prodMap } (g_2 \\circ g_1) = (f_2 \\text{ prodMap } g_2) \\circ (f_1 \\text{ prodMap } g_1). $$$

Lean4

/-- `LinearMap.prodMap` as a `LinearMap` -/
@[simps]
def prodMapLinear [Module S M₃] [Module S M₄] [SMulCommClass R S M₃] [SMulCommClass R S M₄] :
    (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₄) →ₗ[S] M × M₂ →ₗ[R] M₃ × M₄
    where
  toFun f := prodMap f.1 f.2
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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