mulMap_comp_rTensor — Mathlib

English

If M' ≤ M, then composing mulMap M N with the right tensor inclusion equals mulMap M' N.

Русский

Если M' ⊆ M, то композиция mulMap M N с правым тензорным включением равна mulMap M' N.

LaTeX

$$$\forall {M' : Submodule R S}, (M' ≤ M) \Rightarrow mulMap M N \circ (inclusion(hM)).rTensor N = mulMap M' N$$$

Lean4

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

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