Theorems · Definition · linear algebra

Submodule.mulMap

{R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (M N : Submodule R S) → TensorProduct R ↥M ↥N →ₗ[R] S

If M and N are submodules in an algebra S over R, there is the natural R-linear map M ⊗[R] N →ₗ[R] S induced by multiplication in S.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Submodule

Cited by

43 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringAlgebra