Theorems · Theorem · ring theory

Finsupp.mul_sum

∀ {α : Type u_1} {R : Type u_14} {S : Type u_15} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] (b : S) (s : α →₀ R) {f : α → R → S}, b * s.sum f = s.sum fun a c => b * f a c

Defined in

Mathlib.Algebra.BigOperators.Finsupp.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring