eraseLead_add_of_degree_lt_right — Mathlib

English

If deg(p) < deg(q), then (p+q).eraseLead = p + eraseLead(q).

Русский

Если deg(p) < deg(q), то (p+q).eraseLead = p + eraseLead(q).

LaTeX

$$$\deg(p) < \deg(q) \Rightarrow \operatorname{eraseLead}(p+q) = p + \operatorname{eraseLead}(q)$$$

Lean4

theorem eraseLead_add_of_degree_lt_right {p q : R[X]} (pq : p.degree < q.degree) :
    (p + q).eraseLead = p + q.eraseLead := by
  ext n
  by_cases nd : n = q.natDegree
  · rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_right_of_degree_lt pq).symm]
    simpa using (coeff_eq_zero_of_degree_lt (lt_of_lt_of_le pq degree_le_natDegree)).symm
  · rw [eraseLead_coeff, coeff_add, coeff_add, eraseLead_coeff, if_neg, if_neg nd]
    rintro rfl
    exact nd (natDegree_add_eq_right_of_degree_lt pq)

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