Theorems · Definition · linear algebra

TensorProduct.finsuppScalarLeft

(R : Type u_1) →
  [inst : CommSemiring R] →
    (N : Type u_4) →
      [inst_1 : AddCommMonoid N] →
        [inst_2 : Module R N] → (ι : Type u_5) → [DecidableEq ι] → TensorProduct R (ι →₀ R) N ≃ₗ[R] ι →₀ N

The tensor product of ι →₀ R and N is linearly equivalent to ι →₀ N

Defined in

Mathlib.LinearAlgebra.DirectSum.Finsupp

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleDecidableEq