Theorems · Definition · ring theory

SkewPolynomial.update

{R : Type u_1} → [inst : Semiring R] → SkewPolynomial R → ℕ → R → SkewPolynomial R

Replace the coefficient of a p : SkewPolynomial R 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.SkewPolynomial.Basic

Cited by

9 results in Mathlib

Foundations

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

Assumes

Semiring