map_mul — Mathlib

English

The tensor-product map is multiplicative with respect to the multiplication (composition) of endomorphisms in each factor: map(i1 i2; j1 j2) equals map(i1;j1) after map(i2;j2).

Русский

Тензорное отображение сохраняет умножение (иногда композицию) внутри каждой факторной области: отображение от произведения i1 i2 и j1 j2 равно произведению отображений hf(i1, j1) и hf(i2, j2).

LaTeX

$$$ hf.map hf (i_1 i_2) (j_1 j_2) = hf.map hf i_1 j_1 \; hf.map hf i_2 j_2$$$

Lean4

protected theorem map_mul (i₁ i₂ : M₁ →ₗ[R] M₁) (j₁ j₂ : M₂ →ₗ[R] M₂) :
    hf.map hf (i₁ * i₂) (j₁ * j₂) = hf.map hf i₁ j₁ * hf.map hf i₂ j₂ :=
  hf.map_comp hf hf i₁ i₂ j₁ j₂

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