eraseLead_coeff — Mathlib

English

For any i, the i-th coefficient of eraseLead f equals if i equals natDegree(f) then 0 else the i-th coefficient of f.

Русский

Для любого i-i-й коэффициент f.eraseLead равен 0, если i = natDegree(f), иначе — i-й коэффициент f.

LaTeX

$$f.eraseLead.coeff(i) = \begin{cases} 0, & i = f.natDegree \\ f.coeff(i), & \text{otherwise} \end{cases}$$

Lean4

theorem eraseLead_coeff (i : ℕ) : f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i := by
  simp only [eraseLead, coeff_erase]

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