degree_map_le

Mathlib.Algebra.Polynomial.Eval.Degree

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

← MathLib Explorer

English

The degree does not increase under polynomial map: deg(p.map f) ≤ deg p.

Русский

Степень полинома не возрастает после отображения: deg(p.map f) ≤ deg p.

LaTeX

$$$\\deg(p.map f) \\leq \\deg p$$$

Lean4

theorem degree_map_le : degree (p.map f) ≤ 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