leadingCoeff_monic_mul — Mathlib

English

If p is Monic, then leadingCoeff(p q) = leadingCoeff(p) · leadingCoeff(q).

Русский

Если p моничный, то ведущий коэффициент произведения p q равен произведению ведущих коэффициентов.

LaTeX

$$leadingCoeff(p q) = leadingCoeff(p) \cdot leadingCoeff(q)$$

Lean4

theorem leadingCoeff_monic_mul {p q : R[X]} (hp : Monic p) : leadingCoeff (p * q) = leadingCoeff q :=
  by
  rcases eq_or_ne q 0 with (rfl | H)
  · simp
  · rw [leadingCoeff_mul', hp.leadingCoeff, one_mul]
    rwa [hp.leadingCoeff, one_mul, Ne, leadingCoeff_eq_zero]

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