Theorems · Theorem · ring theory

AddMonoidAlgebra.coeff_finsuppSum

∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} {ι : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid N]
  (f : ι →₀ N) (g : ι → N → AddMonoidAlgebra R M), (f.sum g).coeff = f.sum fun i n => (g i n).coeff

Defined in

Mathlib.Algebra.MonoidAlgebra.Defs

Cited by

6 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoid