degree_eq_iff_natDegree_eq_of_pos

Mathlib.Algebra.Polynomial.Degree.Definitions

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

← MathLib Explorer

English

If p ≠ 0, then degree p equals natDegree p cast to WithBot.

Русский

Если p ≠ 0, то degree p равно natDegree p, приведенному к WithBot.

LaTeX

$$$\deg(p) = (\operatorname{natDegree}(p) : \mathrm{WithBot} \mathbb{N})$$$

Lean4

theorem degree_eq_iff_natDegree_eq_of_pos {p : R[X]} {n : ℕ} (hn : 0 < n) : p.degree = n ↔ p.natDegree = n :=
  by
  obtain rfl | h := eq_or_ne p 0
  · simp [hn.ne]
  · exact degree_eq_iff_natDegree_eq h

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

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

Разделы

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

Аффилиация

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