coeff_order — Mathlib

English

If φ ≠ 0, then coeff(φ.order.toNat, φ) ≠ 0.

Русский

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

LaTeX

$$coeff(φ.order.toNat, φ) ≠ 0$$

Lean4

/-- If the order of a formal power series is finite,
then the coefficient indexed by the order is nonzero. -/
theorem coeff_order (h : φ ≠ 0) : coeff φ.order.toNat φ ≠ 0 := by
  classical
  simp only [order, h, not_false_iff, dif_neg]
  generalize_proofs h
  exact Nat.find_spec h

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