map_mul — Mathlib

English

If each endomorphism f_i is multiplied pointwise, the induced map on the tensor product equals the product of the induced maps.

Русский

Если каждая из координатных линейных отображений умножается по соответствию, то полученное отображение на произведении равняется произведению полученных отображений.

LaTeX

$$$\mathrm{map}\big( i \mapsto f_1(i) \cdot f_2(i) \big) = \mathrm{map}\, f_1 \cdot \mathrm{map}\, f_2$$$

Lean4

protected theorem map_mul (f₁ f₂ : Π i, s i →ₗ[R] s i) : map (fun i ↦ f₁ i * f₂ i) = map f₁ * map f₂ :=
  map_comp f₁ f₂

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