degree_pos_of_root

Mathlib.Algebra.Polynomial.Degree.Lemmas

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

← MathLib Explorer

English

If p ≠ 0 and a is a root of p, then degree p > 0.

Русский

Если p ≠ 0 и a является корнем p, то deg p > 0.

LaTeX

$$$0 < \\deg p$$$

Lean4

theorem degree_pos_of_root {p : R[X]} (hp : p ≠ 0) (h : IsRoot p a) : 0 < degree p :=
  lt_of_not_ge fun hlt => by
    have := eq_C_of_degree_le_zero hlt
    rw [IsRoot, this, eval_C] at h
    simp only [h, RingHom.map_zero] at this
    exact hp this

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

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

Разделы

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

Аффилиация

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