int_natDegree

Mathlib.Algebra.Ring.Subring.IntPolynomial

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

English

The natDegree of P.int R hP equals the natDegree of P.

Русский

Порядковый показатель natDegree у P.int R hP равен natDegree у P.

LaTeX

$$$ (P.int R hP).natDegree = P.natDegree$$$

Lean4

@[simp]
theorem int_natDegree : (P.int R hP).natDegree = P.natDegree :=
  rfl

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

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

Разделы

Аффилиация

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