eraseLead_natDegree_lt_or_eraseLead_eq_zero

English

Either (eraseLead f).natDegree < f.natDegree or eraseLead f = 0.

Русский

Либо (eraseLead f).natDegree < natDegree(f), либо eraseLead(f) = 0.

LaTeX

$$$(\operatorname{eraseLead}(f)).\operatorname{natDegree} < \operatorname{natDegree}(f) \ \lor\ \operatorname{eraseLead}(f) = 0$$$

Lean4

theorem eraseLead_natDegree_lt_or_eraseLead_eq_zero (f : R[X]) :
    (eraseLead f).natDegree < f.natDegree ∨ f.eraseLead = 0 :=
  by
  by_cases h : #f.support ≤ 1
  · right
    rw [← C_mul_X_pow_eq_self h]
    simp
  · left
    apply eraseLead_natDegree_lt (lt_of_not_ge h)

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