Theorems · Theorem · general algebraic systems

List.support_sum_eq

∀ {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst_1 : AddZeroClass M] (l : List (ι →₀ M)),
  List.Pairwise (Function.onFun Disjoint Finsupp.support) l →
    l.sum.support = List.foldr (fun x1 x2 => x1.support ⊔ x2) ∅ l

Defined in

Mathlib.Data.Finsupp.BigOperators

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqAddZeroClass