update_zero_eq_erase

Mathlib.Algebra.Polynomial.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.update_zero_eq_erase

English

As a corollary, updating the nth coefficient to zero yields erasing the nth term: p.update n 0 = p.erase n.

Русский

Следствие: обновление n-го коэффициента до нуля равно стиранию n-го терма.

LaTeX

$$$p.update\\ n\\ 0 = p.erase n$$$

Lean4

@[simp]
theorem update_zero_eq_erase (p : R[X]) (n : ℕ) : p.update n 0 = p.erase n :=
  by
  ext
  rw [coeff_update_apply, coeff_erase]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru