order_eq_find' — Mathlib

English

For any p, if there exists a nonzero term, then p.order equals Nat.find hp where hp encodes the existence of a nonzero term.

Русский

Для любого p, если существует ненулевой член, то p.order = Nat.find hp, где hp кодирует существование ненулевого члена.

LaTeX

$$$\\text{order}(p) = \\mathrm{Nat.find}\\, hp$ with\\; hp : \\exists n, p(n) \\neq 0$$

Lean4

theorem order_eq_find' [DecidablePred fun n => p n ≠ 0] (hp : p ≠ 0) :
    p.order = Nat.find (FormalMultilinearSeries.ne_iff.mp hp) :=
  order_eq_find _

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