totalDegree_pow — Mathlib

English

The total degree of a polynomial raised to the n-th power is at most n times the total degree of the polynomial.

Русский

Общая степень полинома в степени n не превышает n раз его общей степени.

LaTeX

$$$\operatorname{totalDegree}(a^{n}) \le n \cdot \operatorname{totalDegree}(a)$$$

Lean4

theorem totalDegree_pow (a : MvPolynomial σ R) (n : ℕ) : (a ^ n).totalDegree ≤ n * a.totalDegree :=
  by
  rw [Finset.pow_eq_prod_const, ← Nat.nsmul_eq_mul, Finset.nsmul_eq_sum_const]
  refine supDegree_prod_le rfl (fun _ _ => ?_)
  exact Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)

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