leadingCoeff_pow_of_pow_leadingCoeff_ne_zero

English

If lc_m(f)^n ≠ 0, then lc_m(f^n) = (lc_m f)^n.

Русский

Если lc_m(f)^n ≠ 0, тогда lc_m(f^n) = (lc_m f)^n.

LaTeX

$$$$ \operatorname{leadingCoeff}_m(f^n) = (\operatorname{leadingCoeff}_m f)^n, \quad \text{provided } \operatorname{leadingCoeff}_m(f)^n \neq 0. $$$$

Lean4

/-- Leading coefficient of powers -/
theorem leadingCoeff_pow_of_pow_leadingCoeff_ne_zero {f : MvPolynomial σ R} {n : ℕ} (hf : m.leadingCoeff f ^ n ≠ 0) :
    m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n := by
  rw [leadingCoeff, degree_pow_of_pow_leadingCoeff_ne_zero hf, coeff_pow_nsmul_degree]

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