eraseLead_add_of_degree_lt_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem eraseLead_add_of_degree_lt_left {p q : R[X]} (pq : q.degree < p.degree) : (p + q).eraseLead = p.eraseLead + q :=
  by
  ext n
  by_cases nd : n = p.natDegree
  · rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_left_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_left_of_degree_lt pq)

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