le_natDegree_of_coe_le_degree

Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

← MathLib Explorer

English

If ↑n ≤ degree(p) then n ≤ natDegree(p).

Русский

Если ↑n ≤ deg(p), то n ≤ natDegree(p).

LaTeX

$$$(\uparrow n \le p.degree) \Rightarrow n \le p.natDegree$$$

Lean4

theorem le_natDegree_of_coe_le_degree (hdeg : ↑n ≤ p.degree) : n ≤ p.natDegree :=
  WithBot.coe_le_coe.mp <| by rwa [degree_eq_natDegree <| ne_zero_of_coe_le_degree hdeg] at hdeg

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

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

Разделы

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

Аффилиация

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