mulMap_comp_lTensor — Mathlib

English

If N' ≤ N, then mulMap M N' equals mulMap M N composed with the left tensor inclusion.

Русский

Если N' ⊆ N, то mulMap M N' = mulMap M N ∘ lTensor включения.

LaTeX

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

Lean4

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

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