monic_of_degree_le_of_coeff_eq_one

Mathlib.Algebra.Polynomial.Degree.Operations

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

← MathLib Explorer

English

If p.degree ≤ n and p.coeff n = 1, then p is Monic.

Русский

Если deg(p) ≤ n и коэффициент при x^n равен 1, тогда p монична.

LaTeX

$$$p.degree \le n \land p.coeff n = 1 \Rightarrow p.Monic$$$

Lean4

theorem monic_of_degree_le_of_coeff_eq_one (n : ℕ) (pn : p.degree ≤ n) (p1 : p.coeff n = 1) : Monic p :=
  monic_of_natDegree_le_of_coeff_eq_one n (natDegree_le_of_degree_le pn) p1

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

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

Разделы

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

Аффилиация

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