leadingCoeff_mul — Mathlib

English

For f,g with f ≠ 0 and lc_m(g) regular, lc_m(fg) = lc_m(f) lc_m(g).

Русский

Для f,g с f ≠ 0 и lc_m(g) регулярным, lc_m(fg) = lc_m(f) lc_m(g).

LaTeX

$$$$ \operatorname{leadingCoeff}_m(fg) = \operatorname{leadingCoeff}_m(f) \cdot \operatorname{leadingCoeff}_m(g). $$$$

Lean4

/-- Multiplicativity of leading coefficients -/
theorem leadingCoeff_mul [IsCancelMulZero R] {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : g ≠ 0) :
    m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g := by
  rw [leadingCoeff, degree_mul hf hg, ← coeff_mul_of_degree_add]

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