leadingCoeff_mul_of_mul_leadingCoeff_ne_zero

English

If the product of leading coefficients is nonzero, then deg(fg) equals deg f plus deg g and the coefficient formula holds.

Русский

Если произведение ведущих коэффициентов не нулевое, то deg(fg) = deg f + deg g и формула коэффициентов справедлива.

LaTeX

$$$m.leadingCoeff f \cdot m.leadingCoeff g \neq 0 \Rightarrow m.degree (f\cdot g) = m.degree f + m.degree g$$$

Lean4

/-- Multiplicativity of leading coefficients -/
theorem leadingCoeff_mul_of_mul_leadingCoeff_ne_zero {f g : MvPolynomial σ R}
    (hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0) : m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g := by
  rw [leadingCoeff, ← coeff_mul_of_degree_add, degree_mul_of_mul_leadingCoeff_ne_zero hfg]

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