coeff_update_same

Mathlib.Algebra.Polynomial.Basic

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

English

The nth coefficient after update equals the given value: (p.update n a).coeff n = a.

Русский

Коэффициент при n после обновления равен a.

LaTeX

$$$(p.update\\ n\\ a).coeff\\ n = a$$$

Lean4

@[simp]
theorem coeff_update_same (p : R[X]) (n : ℕ) (a : R) : (p.update n a).coeff n = a := by
  rw [p.coeff_update_apply, if_pos rfl]

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

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

Разделы

Аффилиация

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