exists_coeff_ne_zero_and_weightedOrder

English

If the weighted order is finite in the sense described by h, there exists d with coeff d f ≠ 0 and weight w d = weightedOrder f.

Русский

Если взвешенный порядок конечен, существует коэффициент d с coeff d f ≠ 0 и weight w d = weightedOrder f.

LaTeX

$$$\exists d,\, coeff d f \neq 0 \land weight w d = f.weightedOrder w$ under suitable hypothesis.$$

Lean4

/-- If the order of a formal power series `f` is finite,
then some coefficient of weight equal to the order of `f` is nonzero. -/
theorem exists_coeff_ne_zero_and_weightedOrder (h : (toNat (f.weightedOrder w) : ℕ∞) = f.weightedOrder w) :
    ∃ d, coeff d f ≠ 0 ∧ weight w d = f.weightedOrder w := by
  classical
  simp_rw [weightedOrder, dif_neg ((ne_zero_iff_weightedOrder_finite w).mpr h), Nat.cast_inj]
  generalize_proofs h1
  exact Nat.find_spec h1

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