isMonicOfDegree_X_pow

Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

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

← MathLib Explorer

English

For any n, X^n is monic of degree n.

Русский

Для любого n, X^n мономичен степени n.

LaTeX

$$$\\\\forall n, IsMonicOfDegree((X : R[X])^n, n)$$$

Lean4

theorem isMonicOfDegree_X_pow (n : ℕ) : IsMonicOfDegree ((X : R[X]) ^ n) n :=
  (isMonicOfDegree_iff ..).mpr ⟨natDegree_X_pow_le n, coeff_X_pow_self n⟩

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

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

Разделы

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

Аффилиация

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