Theorems · Theorem · ring theory

SkewMonoidAlgebra.smul_sum

∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {M : Type u_3} {R : Type u_4} [inst_1 : AddCommMonoid M]
  [inst_2 : DistribSMul R M] {v : SkewMonoidAlgebra k G} {c : R} {h : G → k → M},
  c • v.sum h = v.sum fun a b => c • h a b

Defined in: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommMonoid AddCommMonoid DistribSMul

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

AddCommMonoidstatement and proof · cited by 12,281
SkewMonoidAlgebrastatement and proof · cited by 216
DistribSMulstatement and proof · cited by 117
SkewMonoidAlgebra.sumstatement · cited by 46
Finsupp.smul_sumproof · cited by 11

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.