mulMap_comp_map_inclusion — Mathlib

English

If M', N' are submodules with M' ≤ M and N' ≤ N, then mulMap M N after mapping by inclusion equals mulMap M' N'.

Русский

Если M' ≤ M и N' ≤ N, то mulMap M N после отображения включениями равно mulMap M' N'.

LaTeX

$$$mulMap M N \circ TensorProduct.map (inclusion hM) (inclusion hN) = mulMap M' N'$$$

Lean4

theorem mulMap_comp_map_inclusion {M' N' : Submodule R S} (hM : M' ≤ M) (hN : N' ≤ N) :
    mulMap M N ∘ₗ TensorProduct.map (inclusion hM) (inclusion hN) = mulMap M' N' :=
  TensorProduct.ext' fun _ _ ↦ rfl

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