support_update_ne_zero — Mathlib

English

If a ≠ 0, then the support of p.update n a is the insert of n into the original support: support(p.update n a) = insert n p.support.

Русский

Если a ≠ 0, опора обновления содержит n: support(p.update n a) = insert n p.support.

LaTeX

$$$\\operatorname{support}(p.update n a) = \\operatorname{insert} n \\; \\operatorname{support}(p)$$$

Lean4

theorem support_update_ne_zero (p : R[X]) (n : ℕ) {a : R} (ha : a ≠ 0) : support (p.update n a) = insert n p.support :=
  by classical rw [support_update, if_neg ha]

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