degrees_pow_le

Mathlib.Algebra.MvPolynomial.Degrees

URI: https://scilib.ai/kg/mathlib#MvPolynomial.degrees_pow_le

← MathLib Explorer

English

For a polynomial p and natural number n, deg(p^n) ≤ n · deg(p).

Русский

Для многочлена p и натурального числа n, deg(p^n) ≤ n · deg(p).

LaTeX

$$$\deg(p^n) \le n \cdot \deg(p)$$$

Lean4

theorem degrees_pow_le {p : MvPolynomial σ R} {n : ℕ} : (p ^ n).degrees ≤ n • p.degrees := by
  simpa using degrees_prod_le (s := .range n) (f := fun _ ↦ p)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru