Theorems · Theorem · linear algebra

lsum_comp_mapRange_toSpanSingleton

∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R N] [inst_4 : (m : R) → Decidable (m ≠ 0)] (p : ι → Submodule R N) {v : ι → N}
  (hv : ∀ (i : ι), v i ∈ p i),
  ((DFinsupp.lsum ℕ) fun i => (p i).subtype) ∘ₗ
      (DFinsupp.mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R) =
    Finsupp.linearCombination R v

Combining DFinsupp.lsum with LinearMap.toSpanSingleton is the same as Finsupp.linearCombination

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqSemiringAddCommMonoidModuleDecidable