order_eq_find — Mathlib

English

If there exists a nonzero coefficient, then the order equals the least index at which the coefficient is nonzero, i.e., p.order = Nat.find hp for hp : ∃ n, p n ≠ 0.

Русский

При существовании ненулевого коэффициента порядок равен наименьшему индексу, при котором коэффициент ненулевой: p.order = Nat.find hp.

LaTeX

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

Lean4

theorem order_eq_find [DecidablePred fun n => p n ≠ 0] (hp : ∃ n, p n ≠ 0) : p.order = Nat.find hp := by
  convert Nat.sInf_def hp

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