Theorems · Theorem · commutative algebra

PowerSeries.le_order

∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R) (n : ℕ∞),
  (∀ (i : ℕ), ↑i < n → (PowerSeries.coeff i) φ = 0) → n ≤ φ.order

The order of a formal power series is at least n if the ith coefficient is 0 for all i < n.

Defined in

Mathlib.RingTheory.PowerSeries.Order

Cited by

7 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semiring