natDegree_map_lt

Mathlib.Algebra.Polynomial.Eval.Degree

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

← MathLib Explorer

English

If f(p.leadingCoeff) = 0 and map f p ≠ 0, then natDegree(p.map f) < natDegree p.

Русский

Если f(p.leadingCoeff) = 0 и map f p ≠ 0, то natDegree(p.map f) < natDegree p.

LaTeX

$$$\\operatorname{natDegree}(p.map\\ f) < \\operatorname{natDegree}(p)$$$

Lean4

theorem natDegree_map_lt (hp : f p.leadingCoeff = 0) (hp₀ : map f p ≠ 0) : (p.map f).natDegree < p.natDegree :=
  natDegree_lt_natDegree hp₀ <| degree_map_lt hp <| by rintro rfl; simp at hp₀

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

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

Разделы

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

Аффилиация

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