coeff_eq_zero_of_lt_order — Mathlib

English

If n is below the Hahn series order of A x, then coeff A n x = 0.

Русский

Если n меньше порядка Выражения A x в Hahn серии, то coeff A n x = 0.

LaTeX

$$$n < \mathrm{order}\big((H HahnModule.of R)^{-1}(A x)\big) \Rightarrow coeff\ A\ n\ x = 0$$$

Lean4

theorem coeff_eq_zero_of_lt_order (A : VertexOperator R V) (n : ℤ) (x : V)
    (h : n < HahnSeries.order ((HahnModule.of R).symm (A x))) : coeff A n x = 0 :=
  by
  rw [coeff_eq_ncoeff, ncoeff_eq_zero_of_lt_order A (-n - 1) x]
  cutsat

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