two_le_natDegree_of_nextCoeff_eraseLead

English

If eraseLead f ≠ 0 and f.nextCoeff = 0, then 2 ≤ f.natDegree.

Русский

Если eraseLead(f) ≠ 0 и f.nextCoeff = 0, тогда 2 ≤ natDegree(f).

LaTeX

$$$\operatorname{eraseLead}(f) \neq 0 \land f.nextCoeff = 0 \Rightarrow 2 \le \operatorname{natDegree}(f)$$$

Lean4

theorem two_le_natDegree_of_nextCoeff_eraseLead (hlead : f.eraseLead ≠ 0) (hnext : f.nextCoeff = 0) : 2 ≤ f.natDegree :=
  by
  contrapose! hlead
  rw [Nat.lt_succ_iff, Nat.le_one_iff_eq_zero_or_eq_one, natDegree_eq_zero, natDegree_eq_one] at hlead
  obtain ⟨a, rfl⟩ | ⟨a, ha, b, rfl⟩ := hlead
  · simp
  · rw [nextCoeff_C_mul_X_add_C ha] at hnext
    subst b
    simp

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