Theorems · Theorem · ring theory

MonoidAlgebra.coeff_mul_antidiag

∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Mul M] (x y : MonoidAlgebra 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

1 results in Mathlib

Foundations

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

Assumes

SemiringMul