weightedOrder_le — Mathlib

English

If a coefficient at d is nonzero, then f.weightedOrder w ≤ weight w d.

Русский

Если коэффициент d не нулевой, то взвешенный порядок f ≤ вес коэффициента d.

LaTeX

$$$\text{If } coeff d f \neq 0,\ f.weightedOrder w \le weight w d.$$$

Lean4

/-- If the `d`th coefficient of a formal power series is nonzero,
then the weighted order of the power series is less than or equal to `weight d w`. -/
theorem weightedOrder_le {d : σ →₀ ℕ} (h : coeff d f ≠ 0) : f.weightedOrder w ≤ weight w d :=
  by
  rw [weightedOrder, dif_neg]
  · simp only [ne_eq, Nat.cast_le, Nat.find_le_iff]
    exact ⟨weight w d, le_rfl, d, h, rfl⟩
  · exact (f.ne_zero_iff_exists_coeff_ne_zero_and_weight w).mpr ⟨weight w d, d, h, rfl⟩

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