English
If p.supDegree D = q.supDegree D and p.leadingCoeff D = q.leadingCoeff D, then either (p - q).supDegree D < p.supDegree D or p = q.
Русский
Если степени равны и ведущие коэффициенты равны, то либо (p−q).supDegree D меньше p.supDegree D, либо p = q.
LaTeX
$$$p^{\text{ - } } q^{ } .supDegree D = q.supDegree D \iota p.leadingCoeff D = q.leadingCoeff D \Rightarrow (p - q).supDegree D < p.supDegree D \lor p = q$$$
Lean4
theorem supDegree_sub_lt_of_leadingCoeff_eq (hD : D.Injective) {R} [Ring R] {p q : R[A]}
(hd : p.supDegree D = q.supDegree D) (hc : p.leadingCoeff D = q.leadingCoeff D) :
(p - q).supDegree D < p.supDegree D ∨ p = q :=
by
rw [or_iff_not_imp_right]
refine fun he => (supDegree_sub_le.trans ?_).lt_of_ne ?_
· rw [hd, sup_idem]
· rw [← sub_eq_zero, ← leadingCoeff_eq_zero hD, leadingCoeff] at he
refine fun h => he ?_
rwa [h, Finsupp.sub_apply, ← leadingCoeff, hd, ← leadingCoeff, sub_eq_zero]
