apply_order_ne_zero

Mathlib.Analysis.Calculus.FormalMultilinearSeries

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

English

A variant stating that a nonzero p implies a nonzero coefficient at its order, using a slightly different predicate.

Русский

Вариант утверждения о том, что при p ≠ 0 коэффициент в порядке тоже ненулевой.

LaTeX

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

Lean4

theorem apply_order_ne_zero (hp : p ≠ 0) : p p.order ≠ 0 :=
  Nat.sInf_mem (FormalMultilinearSeries.ne_iff.1 hp)

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

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

Разделы

Аффилиация

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