leadingCoeff_add_of_degree_eq — Mathlib

English

If deg p = deg q and leadingCoeff p + leadingCoeff q ≠ 0, then leadingCoeff(p+q) = leadingCoeff p + leadingCoeff q.

Русский

Если deg p = deg q и сумма ведущих коэффициентов ≠ 0, то leadingCoeff(p+q) = leadingCoeff p + leadingCoeff q.

LaTeX

$$deg(p) = deg(q) \land leadingCoeff(p) + leadingCoeff(q) ≠ 0 \Rightarrow leadingCoeff(p+q) = leadingCoeff(p) + leadingCoeff(q)$$

Lean4

theorem leadingCoeff_add_of_degree_eq (h : degree p = degree q) (hlc : leadingCoeff p + leadingCoeff q ≠ 0) :
    leadingCoeff (p + q) = leadingCoeff p + leadingCoeff q :=
  by
  have : natDegree (p + q) = natDegree p := by
    apply natDegree_eq_of_degree_eq
    rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]
  simp only [leadingCoeff, this, natDegree_eq_of_degree_eq h, coeff_add]

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