add_compLinearMap — Mathlib

English

The sum of two linear maps composed with f equals the sum of their compositions.

Русский

Сумма двух линейных отображений, применённых к f, равна сумме соответствующих композиций.

LaTeX

$$$ (f_1 + f_2).compLinearMap g = f_1.compLinearMap g + f_2.compLinearMap g $$$

Lean4

@[simp]
theorem add_compLinearMap (f₁ f₂ : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) :
    (f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g :=
  by
  ext
  simp only [compLinearMap_apply, add_apply]

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