map_add_right — Mathlib

English

The map is additive in its left argument: map(f1+f2, g) = map(f1,g) + map(f2,g).

Русский

Отображение аддитивно по левому аргументу: map(f1+f2,g) = map(f1,g) + map(f2,g).

LaTeX

$$$\text{map}(f_1+f_2,g) = \text{map}(f_1,g) + \text{map}(f_2,g)$$$

Lean4

theorem map_add_right (f : M →ₗ[A] P) (g₁ g₂ : N →ₗ[R] Q) : map f (g₁ + g₂) = map f g₁ + map f g₂ :=
  by
  ext
  simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul, add_apply, tmul_add]

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