Theorems · Theorem · ring theory

SkewMonoidAlgebra.coeff_sum

∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [inst_1 : AddCommMonoid k']
  {f : SkewMonoidAlgebra k G} {g : G → k → SkewMonoidAlgebra k' G'} {a₂ : G'},
  (f.sum g).coeff a₂ = f.sum fun a₁ b => (g a₁ b).coeff a₂

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoid