Theorems · Definition · field theory

Polynomial.update

{R : Type u} → [inst : Semiring R] → Polynomial R → ℕ → R → Polynomial R

Replace the coefficient of a p : R[X] at a given degree n : ℕ by a given value a : R. If a = 0, this is equal to p.erase n If p.natDegree < n and a ≠ 0, this increases the degree to n.

Defined in

Mathlib.Algebra.Polynomial.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

Semiring