leadingCoeff_add_eq_left — Mathlib

English

If q.supDegree D < p.supDegree D and D injective, then (p+q).leadingCoeff D = p.leadingCoeff D.

Русский

Если q.supDegree D < p.supDegree D и D инъективна, то ведущий коэффициент суммы равен ведущему коэффициенту p.

LaTeX

$$$ (p + q).leadingCoeff D = p.leadingCoeff D $ при $ q.supDegree D < p.supDegree D$$$

Lean4

theorem leadingCoeff_add_eq_left (h : q.supDegree D < p.supDegree D) : (p + q).leadingCoeff D = p.leadingCoeff D :=
  by
  obtain ⟨a, he⟩ := supDegree_mem_range D (ne_zero_of_not_supDegree_le h.not_ge)
  rw [leadingCoeff, supDegree_add_eq_left h, Finsupp.add_apply, ← leadingCoeff,
    apply_eq_zero_of_not_le_supDegree (D := D), add_zero]
  rw [← he, Function.apply_invFun_apply (f := D), he]; exact h.not_ge

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