Theorems · Theorem · ring theory

AddMonoidAlgebra.coeff_mul_single_of_forall_add_ne

∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {m m' : M} [inst_1 : Add M] (r : R) (x : AddMonoidAlgebra R M),
  (∀ (d : M), d + m ≠ m') → (x * AddMonoidAlgebra.single m r).coeff m' = 0

Defined in

Mathlib.Algebra.MonoidAlgebra.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringAdd