nextCoeff_ne_zero

Mathlib.Algebra.Polynomial.Degree.Definitions

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

English

NextCoeff(p) ≠ 0 iff natDegree(p) ≠ 0 and coeff(natDegree(p) − 1) ≠ 0.

Русский

NextCoeff(p) ≠ 0 тогда и только тогда, когда natDegree(p) ≠ 0 и coeff(natDegree(p) − 1) ≠ 0.

LaTeX

$$$ p.nextCoeff \neq 0 \iff p.natDegree \neq 0 \land p.coeff(p.natDegree - 1) \neq 0 $$$

Lean4

theorem nextCoeff_ne_zero : p.nextCoeff ≠ 0 ↔ p.natDegree ≠ 0 ∧ p.coeff (p.natDegree - 1) ≠ 0 := by simp [nextCoeff]

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

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

Разделы

Аффилиация

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