Theorems · Theorem · ring theory

SkewMonoidAlgebra.coeff_mul

∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : SMulZeroClass G k]
  [inst_3 : DecidableEq G] (f g : SkewMonoidAlgebra k G) (x : G),
  (f * g).coeff x = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

9 results in Mathlib

Foundations

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

Assumes

SemiringMulSMulZeroClassDecidableEq