erase_monomial — Mathlib

English

The coefficients of p.update n a are obtained by updating the nth component of the coefficient sequence p.coeff by a, i.e. (p.update n a).coeff = Function.update p.coeff n a.

Русский

Коэффициенты p.update n a получаются путём обновления n-го элемента последовательности коэффициентов p: (p.update n a).coeff = Function.update p.coeff n a.

LaTeX

$$$(p.update\\ n\\ a).coeff = \\text{Function.update}(p.coeff, n, a)$$$

Lean4

@[simp]
theorem erase_monomial {n : ℕ} {a : R} : erase n (monomial n a) = 0 :=
  toFinsupp_injective <| by simp

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