Theorems · Theorem · ring theory

Finsupp.sum_mul

∀ {α : 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}, s.sum f * b = s.sum fun a c => f a c * b

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