leadingCoeff_eq_zero — Mathlib

English

Let p be a polynomial. Then p is identically zero if and only if its leading coefficient is zero.

Русский

Пусть p — многочлен. Тогда p равен нулю тогда и только тогда, когда его ведущий коэффициент равен нулю.

LaTeX

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

Lean4

@[simp]
theorem leadingCoeff_eq_zero : leadingCoeff p = 0 ↔ p = 0 :=
  ⟨fun h =>
    Classical.by_contradiction fun hp =>
      mt mem_support_iff.1 (Classical.not_not.2 h) (mem_of_max (degree_eq_natDegree hp)),
    fun h => h.symm ▸ leadingCoeff_zero⟩

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