degree_smul_le

Mathlib.Algebra.Polynomial.Degree.Operations

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

← MathLib Explorer

English

Scalar multiplication does not increase the degree of a polynomial.

Русский

Умножение на скаляр не увеличивает степень многочлена.

LaTeX

$$$ \deg(a \cdot p) \leq \deg(p).$$$

Lean4

theorem degree_smul_le {S : Type*} [SMulZeroClass S R] (a : S) (p : R[X]) : degree (a • p) ≤ degree p :=
  by
  refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
  rw [degree_lt_iff_coeff_zero] at hm
  simp [hm m le_rfl]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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