leadingCoeff_eq_zero_iff_deg_eq_bot

Mathlib.Algebra.Polynomial.Degree.Definitions

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

English

The leading coefficient of p is zero if and only if the degree of p is the bottom element.

Русский

Ведущий коэффициент p равен нулю тогда и только тогда, когда степень p равна ⊥.

LaTeX

$$$\operatorname{leadingCoeff}(p) = 0 \iff \deg(p) = \bot$$$

Lean4

theorem leadingCoeff_eq_zero_iff_deg_eq_bot : leadingCoeff p = 0 ↔ degree p = ⊥ := by
  rw [leadingCoeff_eq_zero, degree_eq_bot]

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

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

Разделы

Аффилиация

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