English
A basic simplification lemma linking supDegree with support properties; the precise formal statement is a technical equality about membership of the support under multiplication.
Русский
Базовая вспомогательная лемма, связывающая supDegree с свойствами поддержки; точное утверждение — техническое равенство о принадлежности поддержки при умножении.
LaTeX
$$$$\text{(technical equality about } \operatorname{supDegree} \text{ and } \operatorname{support} \text{ is omitted here in plain text).}$$$$
Lean4
theorem leadingCoeff_mul_eq_right (hD : D.Injective) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) (hp : p.Monic D) :
(p * q).leadingCoeff D = q.leadingCoeff D :=
by
obtain rfl | hq := eq_or_ne q 0
· rw [mul_zero]
rw [leadingCoeff, hp.supDegree_mul_of_ne_zero_right hD hadd hq, apply_supDegree_add_supDegree hD hadd, hp, one_mul]
