degree_eq_of_le_of_coeff_ne_zero'

Mathlib.Tactic.ComputeDegree

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.ComputeDegree.degree_eq_of_le_of_coeff_ne_zero'

Lean4

theorem degree_eq_of_le_of_coeff_ne_zero' {deg m o : WithBot ℕ} {c : R} {p : R[X]} (h_deg_le : degree p ≤ m)
    (coeff_eq : coeff p (WithBot.unbotD 0 deg) = c) (coeff_ne_zero : c ≠ 0) (deg_eq_deg : m = deg)
    (coeff_eq_deg : o = deg) : degree p = deg :=
  by
  subst coeff_eq coeff_eq_deg deg_eq_deg
  rcases eq_or_ne m ⊥ with rfl | hh
  · exact bot_unique h_deg_le
  · obtain ⟨m, rfl⟩ := WithBot.ne_bot_iff_exists.mp hh
    exact degree_eq_of_le_of_coeff_ne_zero ‹_› ‹_›

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

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

Разделы

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

Аффилиация

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