update — Mathlib

English

If i ≠ n, then the i-th coefficient remains unchanged: (p.update n a).coeff i = p.coeff i.

Русский

Если i ≠ n, i-й коэффициент не меняется: (p.update n a).coeff i = p.coeff i.

LaTeX

$$$i \\neq n \\Rightarrow (p.update\\ n\\ a).coeff\\ i = p.coeff\\ i$$$

Lean4

/-- 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`. -/
def update (p : R[X]) (n : ℕ) (a : R) : R[X] :=
  Polynomial.ofFinsupp (p.toFinsupp.update n a)

Похожие утверждения