English
Under NoZeroDivisors on R and the usual injectivity/additivity hypotheses for D, the leading coefficient is multiplicative: leadingCoeff_D(p q) = leadingCoeff_D(p) · leadingCoeff_D(q).
Русский
При отсутствии делителей нуля в R и стандартных предположениях на D, ведущий коэффициент умножается: leadingCoeff_D(p q) = leadingCoeff_D(p) · leadingCoeff_D(q).
LaTeX
$$$$\operatorname{leadingCoeff}_D(p q) = \operatorname{leadingCoeff}_D(p) \cdot \operatorname{leadingCoeff}_D(q).$$$$
Lean4
theorem leadingCoeff_mul [NoZeroDivisors R] (hD : D.Injective) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) :
(p * q).leadingCoeff D = p.leadingCoeff D * q.leadingCoeff D :=
by
obtain rfl | hp := eq_or_ne p 0
· simp_rw [leadingCoeff_zero, zero_mul, leadingCoeff_zero]
obtain rfl | hq := eq_or_ne q 0
· simp_rw [leadingCoeff_zero, mul_zero, leadingCoeff_zero]
rw [← apply_supDegree_add_supDegree hD hadd, ← supDegree_mul hD hadd ?_ hp hq, leadingCoeff]
apply mul_ne_zero <;> rwa [Ne, leadingCoeff_eq_zero hD]
