ne_zero

Mathlib.Algebra.Polynomial.Sequence

URI: https://scilib.ai/kg/mathlib#Polynomial.Sequence.ne_zero

English

No polynomial in the sequence is zero: S i ≠ 0 for all i.

Русский

Ни один элемент последовательности не равен нулю: S_i ≠ 0 для всех i.

LaTeX

$$$\forall i\in\mathbb{N},\; S(i) \neq 0$$$

Lean4

/-- No polynomial in the sequence is zero. -/
@[simp]
theorem ne_zero (i : ℕ) : S i ≠ 0 :=
  degree_ne_bot.mp <| by simp [S.degree_eq i]

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

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

Разделы

Аффилиация

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