degree_pow_le — Mathlib

English

For any polynomial f and natural number n, the degree of f^n does not exceed n times the degree of f with respect to m: deg_m(f^n) ≼_m n · deg_m(f).

Русский

Для любого полинома f и натурального числа n степень f^n по отношению к m не превосходит n умноженное на deg_m(f).

LaTeX

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

Lean4

/-- Monomial degree of powers -/
theorem degree_pow_le {f : MvPolynomial σ R} (n : ℕ) : m.degree (f ^ n) ≼[m] n • (m.degree f) := by
  induction n with
  | zero => simp [m.degree_one]
  | succ n hrec =>
    simp only [pow_add, pow_one, add_smul, one_smul]
    apply le_trans m.degree_mul_le
    simp only [map_add, add_le_add_iff_right]
    exact hrec

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