nextCoeff_eq_zero — Mathlib

English

NextCoeff(p) equals zero iff either natDegree(p) = 0 or natDegree(p) > 0 and the coefficient of natDegree(p) − 1 is zero.

Русский

NextCoeff(p) равно нулю тогда и только тогда, когда или natDegree(p) = 0 или natDegree(p) > 0 и коэффициент при natDegree(p) − 1 равен нулю.

LaTeX

$$$ p.nextCoeff = 0 \iff p.natDegree = 0 \lor \big(0 < p.natDegree \land p.coeff(p.natDegree - 1) = 0\big) $$$

Lean4

theorem nextCoeff_eq_zero : p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0 := by
  simp [nextCoeff, or_iff_not_imp_left, pos_iff_ne_zero]; simp_all

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