Theorems · Definition · linear algebra

Submodule.mulLeftMap

{R : Type u_1} →
  [inst : Semiring R] →
    {S : Type u_4} →
      [inst_1 : Semiring S] →
        [inst_2 : Module R S] →
          [SMulCommClass R R S] →
            [SMulCommClass R S S] →
              {M : Submodule R S} → (N : Submodule R S) → {ι : Type u_5} → (ι → ↥M) → (ι →₀ ↥N) →ₗ[R] S

If M and N are submodules of an R-algebra S, m : ι → M is a family of elements, then there is an R-linear map from ι →₀ N to S which maps { n_i } to the sum of m_i * n_i. This is used in the definition of linearly disjointness.

Defined in

Mathlib.LinearAlgebra.Finsupp.LSum

Cited by

12 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringSemiringModuleSMulCommClassSMulCommClass