order_eq_zero_iff

Mathlib.Analysis.Calculus.FormalMultilinearSeries

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

English

If p ≠ 0, then the coefficient at the order is nonzero: p(p.order) ≠ 0.

Русский

Если p ≠ 0, то коэффициент при порядке не равен нулю: p(p.order) ≠ 0.

LaTeX

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

Lean4

theorem order_eq_zero_iff (hp : p ≠ 0) : p.order = 0 ↔ p 0 ≠ 0 := by simp [order_eq_zero_iff', hp]

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

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

Разделы

Аффилиация

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