Theorems · Theorem · ring theory

SkewMonoidAlgebra.sum_mul

∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {S : Type u_3} [inst_1 : NonUnitalNonAssocSemiring S] (b : S)
  (s : SkewMonoidAlgebra k G) {f : G → k → S}, s.sum f * b = s.sum fun a c => f a c * b

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoidNonUnitalNonAssocSemiring