leadingCoeff_mul_monic — Mathlib

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]

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