English
For any polynomials p, q, if q is Monic, then leadingCoeff(p q) = leadingCoeff(p).
Русский
Для любых полиномов p, q, если q моничен, то ведущий коэффициент произведения равен ведущему коэффициенту p.
LaTeX
$$leadingCoeff(p q) = leadingCoeff(p) when q.Monic$$
Lean4
theorem leadingCoeff_mul_monic {p q : R[X]} (hq : Monic q) : leadingCoeff (p * q) = leadingCoeff p :=
letI := Classical.decEq R
Decidable.byCases (fun H : leadingCoeff p = 0 => by rw [H, leadingCoeff_eq_zero.1 H, zero_mul, leadingCoeff_zero])
fun H : leadingCoeff p ≠ 0 => by
rw [leadingCoeff_mul', hq.leadingCoeff, mul_one]
rwa [hq.leadingCoeff, mul_one]