natDegree_pow

Mathlib.Algebra.Polynomial.Degree.Domain

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

← MathLib Explorer

English

natDegree(p^n) = n · natDegree(p).

Русский

natDegree(p^n) = n · natDegree(p).

LaTeX

$$natDegree(p^n) = n · natDegree(p)$$

Lean4

@[simp]
theorem natDegree_pow (p : R[X]) (n : ℕ) : natDegree (p ^ n) = n * natDegree p := by
  classical
  obtain rfl | hp := eq_or_ne p 0
  · obtain rfl | hn := eq_or_ne n 0 <;> simp [*]
  exact natDegree_pow' <| by rw [← leadingCoeff_pow, Ne, leadingCoeff_eq_zero]; exact pow_ne_zero _ hp

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

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

Разделы

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

Аффилиация

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