Theorems · Theorem · commutative algebra

MvPolynomial.coeff_single_X_pow

∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (s s' : σ) (n n' : ℕ),
  MvPolynomial.coeff (fun₀ | s' => n') (MvPolynomial.X s ^ n) = if s = s' ∧ n = n' ∨ n = 0 ∧ n' = 0 then 1 else 0

Defined in

Mathlib.Algebra.MvPolynomial.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringDecidableEq