natDegree_eq_of_degree_eq

Mathlib.Algebra.Polynomial.Degree.Definitions

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

English

If p ≠ 0, then degree(p) equals natDegree(p) cast.

Русский

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

LaTeX

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

Lean4

theorem natDegree_eq_of_degree_eq [Semiring S] {q : S[X]} (h : degree p = degree q) : natDegree p = natDegree q := by
  unfold natDegree; rw [h]

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

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

Разделы

Аффилиация

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