ne_zero_of_order_ne_zero

Mathlib.Analysis.Calculus.FormalMultilinearSeries

URI: https://scilib.ai/kg/mathlib#FormalMultilinearSeries.ne_zero_of_order_ne_zero

English

If p is nonzero, then its order is the first index where p(n) ≠ 0, i.e., p(p.order) ≠ 0.

Русский

Если p ≠ 0, то p(p.order) ≠ 0, поскольку p‑order — первый индекс с ненулевым членом.

LaTeX

$$$p \\neq 0 \\Rightarrow p(p.\\mathrm{order}) \\neq 0$$$

Lean4

theorem ne_zero_of_order_ne_zero (hp : p.order ≠ 0) : p ≠ 0 := fun h => by simp [h] at hp

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

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

Разделы

Аффилиация

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