degree_smul_le

Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

← MathLib Explorer

English

For any scalar r and polynomial f, deg_m(r · f) ≤ deg_m(f).

Русский

Для скаляра r и полинома f верно deg_m(r · f) ≤ deg_m(f).

LaTeX

$$$$ \deg_m(r \cdot f) \preceq_m \deg_m(f). $$$$

Lean4

theorem degree_smul_le {r : R} {f : MvPolynomial σ R} : m.degree (r • f) ≼[m] m.degree f :=
  by
  rw [smul_eq_C_mul]
  apply le_of_le_of_eq degree_mul_le
  simp

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

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

Разделы

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

Аффилиация

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