degree_pow

Mathlib.Algebra.Polynomial.Degree.Operations

URI: https://scilib.ai/kg/mathlib#Polynomial.degree_pow

English

For any polynomial p and natural number n, the degree of the nth power equals n times the degree of p: deg(p^n) = n · deg(p).

Русский

Для любого многочлена p и натурального числа n степень deg(p^n) равна n раз deg(p).

LaTeX

$$$\deg(p^n)=n\cdot\deg(p).$$$

Lean4

@[simp]
theorem degree_pow [Nontrivial R] (p : R[X]) (n : ℕ) : degree (p ^ n) = n • degree p :=
  map_pow (@degreeMonoidHom R _ _ _) _ _

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

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

Разделы

Аффилиация

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