mapBilinear_apply — Mathlib

English

Tensor product map distributes over addition on the left: map (f1 + f2) g = map f1 g + map f2 g.

Русский

Тензорное отображение распределяется по сумме слева: map (f1 + f2) g = map f1 g + map f2 g.

LaTeX

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

Lean4

@[simp]
theorem mapBilinear_apply (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : mapBilinear R M N P Q f g = map f g :=
  rfl

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