natDegree_sub

Mathlib.Algebra.Polynomial.Degree.Lemmas

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

English

The natDegree of p − q equals the natDegree of q − p.

Русский

natDegree( p − q ) = natDegree( q − p ).

LaTeX

$$$\operatorname{natDegree}(p - q) = \operatorname{natDegree}(q - p)$$$

Lean4

theorem natDegree_sub : (p - q).natDegree = (q - p).natDegree := by rw [← natDegree_neg, neg_sub]

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

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

Разделы

Аффилиация

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