leadingCoeff_eraseLead_eq_nextCoeff

English

If f.nextCoeff ≠ 0 then eraseLead f leadingCoeff equals f.nextCoeff.

Русский

Если f.nextCoeff ≠ 0, то leadingCoeff(eraseLead(f)) = f.nextCoeff.

LaTeX

$$$\, f.nextCoeff \neq 0 \Rightarrow \operatorname{leadingCoeff}(\operatorname{eraseLead}(f)) = f.nextCoeff$$$

Lean4

theorem leadingCoeff_eraseLead_eq_nextCoeff (h : f.nextCoeff ≠ 0) : f.eraseLead.leadingCoeff = f.nextCoeff :=
  by
  have := natDegree_pos_of_nextCoeff_ne_zero h
  rw [leadingCoeff, nextCoeff, natDegree_eraseLead h, if_neg, eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne]
  all_goals positivity

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