Theorems · Theorem · ring theory

AddMonoidAlgebra.mul_apply_antidiagonal

Deprecated since 2026-06-18Use AddMonoidAlgebra.coeff_mul_antidiag instead.

∀ {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

Alias of AddMonoidAlgebra.coeff_mul_antidiag.

Defined in

Mathlib.Algebra.MonoidAlgebra.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringAdd