degree_pow — Mathlib

English

In a reduced ring, for any polynomial f and natural n, deg_m(f^n) = n · deg_m(f).

Русский

В уменьшенном кольце для любого полинома f и натурального n выполняется deg_m(f^n) = n · deg_m(f).

LaTeX

$$$$ \deg_m(f^n) = n \cdot \deg_m(f). $$$$

Lean4

/-- Monomial degree of powers (in a reduced ring) -/
theorem degree_pow [IsReduced R] (f : MvPolynomial σ R) (n : ℕ) : m.degree (f ^ n) = n • m.degree f :=
  by
  by_cases hf : f = 0
  · rw [hf, degree_zero, smul_zero]
    by_cases hn : n = 0
    · rw [hn, pow_zero, degree_one]
    · rw [zero_pow hn, degree_zero]
  nontriviality R
  apply degree_pow_of_pow_leadingCoeff_ne_zero
  apply IsReduced.pow_ne_zero
  rw [leadingCoeff_ne_zero_iff]
  exact hf

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