natDegree_C_mul_le

Mathlib.Algebra.Polynomial.Degree.Lemmas

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

English

natDegree_mul_C_le: For any f and a, natDegree(f · C a) ≤ natDegree f.

Русский

natDegree(f · C a) ≤ natDegree f для любых f и a.

LaTeX

$$$\\operatorname{natDegree}(\\,f \\cdot C a\\,) \\le \\operatorname{natDegree}(f)$$$

Lean4

theorem natDegree_C_mul_le (a : R) (f : R[X]) : (C a * f).natDegree ≤ f.natDegree := by
  simpa using natDegree_mul_le (p := C a)

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

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

Разделы

Аффилиация

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