erase_same — Mathlib

English

For all p, n, a, i, the nth coefficient of p.update n a equals a if i = n, and equals p.coeff i otherwise.

Русский

Для всех p, n, a, i коэффициент i в p.update n a равен a, если i = n, и равен p.coeff i, если i ≠ n.

LaTeX

$$$(p.update\\ n\\ a).coeff\\ i = \\begin{cases} a, & i = n, \\\\ p.coeff\\ i, & i \\neq n. \\end{cases}$$$

Lean4

@[simp]
theorem erase_same (p : R[X]) (n : ℕ) : coeff (p.erase n) n = 0 := by simp [coeff_erase]

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