supDegree_mem_support — Mathlib

English

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

Русский

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

LaTeX

$$$p.supDegree D < q.supDegree D \Rightarrow (p + q).leadingCoeff D = q.leadingCoeff D$$$

Lean4

theorem supDegree_mem_support (hD : D.Injective) (hp : p ≠ 0) : D.invFun (p.supDegree D) ∈ p.support :=
  by
  obtain ⟨a, ha, he⟩ := exists_supDegree_mem_support D hp
  rwa [he, Function.leftInverse_invFun hD]

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