eraseLead_coeff_of_ne

Mathlib.Algebra.Polynomial.EraseLead

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

English

If i ≠ natDegree(f), then eraseLead f has the same i-th coefficient as f.

Русский

Если i ≠ natDegree(f), то i-й коэффициент f.eraseLead равен коэффициенту f.

LaTeX

$$f.eraseLead.coeff(i) = f.coeff(i) \quad \text{if } i \neq f.natDegree$$

Lean4

theorem eraseLead_coeff_of_ne (i : ℕ) (hi : i ≠ f.natDegree) : f.eraseLead.coeff i = f.coeff i := by
  simp [eraseLead_coeff, hi]

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

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

Разделы

Аффилиация

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