leadingCoeff_sub_of_degree_eq — Mathlib

English

If natDegree p < natDegree q, then natDegree(p − q) = natDegree q.

Русский

Если natDegree(p) < natDegree(q), то natDegree(p − q) = natDegree(q).

LaTeX

$$$\operatorname{natDegree}(p - q) = \operatorname{natDegree}(q) \quad\text{if } \operatorname{natDegree}(p) < \operatorname{natDegree}(q)$$$

Lean4

theorem leadingCoeff_sub_of_degree_eq (h : degree p = degree q) (hlc : leadingCoeff p ≠ leadingCoeff q) :
    leadingCoeff (p - q) = leadingCoeff p - leadingCoeff q :=
  by
  replace h : degree p = degree (-q) := by rwa [q.degree_neg]
  replace hlc : leadingCoeff p + leadingCoeff (-q) ≠ 0 := by
    rwa [← sub_ne_zero, sub_eq_add_neg, ← q.leadingCoeff_neg] at hlc
  rw [sub_eq_add_neg, leadingCoeff_add_of_degree_eq h hlc, leadingCoeff_neg, sub_eq_add_neg]

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