Theorems · Theorem · ring theory

AddMonoidAlgebra.coeff_mul_antidiag

∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Add M] (x y : AddMonoidAlgebra R M) (m : M)
  (s : Finset (M × M)), (∀ {p : M × M}, p ∈ s ↔ p.1 + p.2 = m) → (x * y).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2

Defined in

Mathlib.Algebra.MonoidAlgebra.Defs

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringAdd