Theorems · Theorem · commutative algebra

Polynomial.eval_eq_sum_degreeLTEquiv

∀ {R : Type u} [inst : Semiring R] {n : ℕ} {p : Polynomial R} (hp : p ∈ Polynomial.degreeLT R n) (x : R),
  Polynomial.eval x p = ∑ i, (Polynomial.degreeLTEquiv R n) ⟨p, hp⟩ i * x ^ ↑i

Defined in

Mathlib.RingTheory.Polynomial.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

Semiring