natDegree_mul_C_of_isUnit

Mathlib.Algebra.Polynomial.Degree.Operations

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

English

For any unit a, natDegree(p) equals natDegree(p * C(a)).

Русский

Для любого единичного a натуральная степень p равна natDegree(p * C(a)).

LaTeX

$$natDegree(p * C(a)) = natDegree(p) при IsUnit(a)$$

Lean4

theorem natDegree_mul_C_of_isUnit (ha : IsUnit a) (p : R[X]) : (p * C a).natDegree = p.natDegree := by
  simp [natDegree, degree_mul_C_of_isUnit ha]

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

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

Разделы

Аффилиация

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