degree_ne_of_natDegree_ne

Mathlib.Algebra.Polynomial.Degree.Definitions

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

English

If p.natDegree ≠ n, then degree p ≠ n.

Русский

Если p.natDegree ≠ n, тогда degree(p) ≠ n.

LaTeX

$$$\operatorname{natDegree}(p) \neq n \;\Rightarrow\; \deg(p) \neq n$$$

Lean4

theorem degree_ne_of_natDegree_ne {n : ℕ} : p.natDegree ≠ n → degree p ≠ n :=
  mt natDegree_eq_of_degree_eq_some

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

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

Разделы

Аффилиация

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