Documentation

Mathlib.RingTheory.PowerSeries.Order

Formal power series (in one variable) - Order #

The PowerSeries.order of a formal power series φ is the multiplicity of the variable X in φ.

If the coefficients form an integral domain, then PowerSeries.order is an additive valuation (PowerSeries.order_mul, PowerSeries.le_order_add).

We prove that if the commutative ring R of coefficients is an integral domain, then the ring R⟦X⟧ of formal power series in one variable over R is an integral domain.

Given a non-zero power series f, divided_by_X_pow_order f is the power series obtained by dividing out the largest power of X that divides f, that is its order. This is useful when proving that R⟦X⟧ is a normalization monoid, which is done in PowerSeries.Inverse.

theorem PowerSeries.exists_coeff_ne_zero_iff_ne_zero {R : Type u_1} [Semiring R] {φ : PowerSeries R} :
(∃ (n : ), (PowerSeries.coeff R n) φ 0) φ 0
def PowerSeries.order {R : Type u_1} [Semiring R] (φ : PowerSeries R) :

The order of a formal power series φ is the greatest n : PartENat such that X^n divides φ. The order is if and only if φ = 0.

Equations
Instances For
    @[simp]

    The order of the 0 power series is infinite.

    theorem PowerSeries.order_finite_iff_ne_zero {R : Type u_1} [Semiring R] {φ : PowerSeries R} :
    φ.order.Dom φ 0
    theorem PowerSeries.coeff_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} (h : φ.order.Dom) :
    (PowerSeries.coeff R (φ.order.get h)) φ 0

    If the order of a formal power series is finite, then the coefficient indexed by the order is nonzero.

    theorem PowerSeries.order_le {R : Type u_1} [Semiring R] {φ : PowerSeries R} (n : ) (h : (PowerSeries.coeff R n) φ 0) :
    φ.order n

    If the nth coefficient of a formal power series is nonzero, then the order of the power series is less than or equal to n.

    theorem PowerSeries.coeff_of_lt_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} (n : ) (h : n < φ.order) :
    (PowerSeries.coeff R n) φ = 0

    The nth coefficient of a formal power series is 0 if n is strictly smaller than the order of the power series.

    @[simp]
    theorem PowerSeries.order_eq_top {R : Type u_1} [Semiring R] {φ : PowerSeries R} :
    φ.order = φ = 0

    The 0 power series is the unique power series with infinite order.

    theorem PowerSeries.nat_le_order {R : Type u_1} [Semiring R] (φ : PowerSeries R) (n : ) (h : i < n, (PowerSeries.coeff R 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.

    theorem PowerSeries.le_order {R : Type u_1} [Semiring R] (φ : PowerSeries R) (n : PartENat) (h : ∀ (i : ), i < n(PowerSeries.coeff R 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.

    theorem PowerSeries.order_eq_nat {R : Type u_1} [Semiring R] {φ : PowerSeries R} {n : } :
    φ.order = n (PowerSeries.coeff R n) φ 0 i < n, (PowerSeries.coeff R i) φ = 0

    The order of a formal power series is exactly n if the nth coefficient is nonzero, and the ith coefficient is 0 for all i < n.

    theorem PowerSeries.order_eq {R : Type u_1} [Semiring R] {φ : PowerSeries R} {n : PartENat} :
    φ.order = n (∀ (i : ), i = n(PowerSeries.coeff R i) φ 0) ∀ (i : ), i < n(PowerSeries.coeff R i) φ = 0

    The order of a formal power series is exactly n if the nth coefficient is nonzero, and the ith coefficient is 0 for all i < n.

    theorem PowerSeries.le_order_add {R : Type u_1} [Semiring R] (φ : PowerSeries R) (ψ : PowerSeries R) :
    min φ.order ψ.order (φ + ψ).order

    The order of the sum of two formal power series is at least the minimum of their orders.

    theorem PowerSeries.order_add_of_order_eq {R : Type u_1} [Semiring R] (φ : PowerSeries R) (ψ : PowerSeries R) (h : φ.order ψ.order) :
    (φ + ψ).order = φ.order ψ.order

    The order of the sum of two formal power series is the minimum of their orders if their orders differ.

    theorem PowerSeries.order_mul_ge {R : Type u_1} [Semiring R] (φ : PowerSeries R) (ψ : PowerSeries R) :
    φ.order + ψ.order (φ * ψ).order

    The order of the product of two formal power series is at least the sum of their orders.

    theorem PowerSeries.order_monomial {R : Type u_1} [Semiring R] (n : ) (a : R) [Decidable (a = 0)] :
    ((PowerSeries.monomial R n) a).order = if a = 0 then else n

    The order of the monomial a*X^n is infinite if a = 0 and n otherwise.

    theorem PowerSeries.order_monomial_of_ne_zero {R : Type u_1} [Semiring R] (n : ) (a : R) (h : a 0) :
    ((PowerSeries.monomial R n) a).order = n

    The order of the monomial a*X^n is n if a ≠ 0.

    theorem PowerSeries.coeff_mul_of_lt_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} {ψ : PowerSeries R} {n : } (h : n < ψ.order) :
    (PowerSeries.coeff R n) (φ * ψ) = 0

    If n is strictly smaller than the order of ψ, then the nth coefficient of its product with any other power series is 0.

    theorem PowerSeries.coeff_mul_one_sub_of_lt_order {R : Type u_2} [CommRing R] {φ : PowerSeries R} {ψ : PowerSeries R} (n : ) (h : n < ψ.order) :
    (PowerSeries.coeff R n) (φ * (1 - ψ)) = (PowerSeries.coeff R n) φ
    theorem PowerSeries.coeff_mul_prod_one_sub_of_lt_order {R : Type u_2} {ι : Type u_3} [CommRing R] (k : ) (s : Finset ι) (φ : PowerSeries R) (f : ιPowerSeries R) :
    (is, k < (f i).order)(PowerSeries.coeff R k) (φ * is, (1 - f i)) = (PowerSeries.coeff R k) φ
    theorem PowerSeries.X_pow_order_dvd {R : Type u_1} [Semiring R] {φ : PowerSeries R} (h : φ.order.Dom) :
    PowerSeries.X ^ φ.order.get h φ
    theorem PowerSeries.order_eq_multiplicity_X {R : Type u_2} [Semiring R] [DecidableRel fun (x x_1 : PowerSeries R) => x x_1] (φ : PowerSeries R) :
    φ.order = multiplicity PowerSeries.X φ

    Given a non-zero power series f, divided_by_X_pow_order f is the power series obtained by dividing out the largest power of X that divides f, that is its order

    Equations
    Instances For
      theorem PowerSeries.self_eq_X_pow_order_mul_divided_by_X_pow_order {R : Type u_1} [Semiring R] {f : PowerSeries R} (hf : f 0) :
      PowerSeries.X ^ f.order.get * PowerSeries.divided_by_X_pow_order hf = f
      @[simp]

      The order of the formal power series 1 is 0.

      theorem PowerSeries.order_zero_of_unit {R : Type u_1} [Semiring R] [Nontrivial R] {f : PowerSeries R} :
      IsUnit ff.order = 0

      The order of an invertible power series is 0.

      @[simp]
      theorem PowerSeries.order_X {R : Type u_1} [Semiring R] [Nontrivial R] :
      PowerSeries.X.order = 1

      The order of the formal power series X is 1.

      @[simp]
      theorem PowerSeries.order_X_pow {R : Type u_1} [Semiring R] [Nontrivial R] (n : ) :
      (PowerSeries.X ^ n).order = n

      The order of the formal power series X^n is n.

      theorem PowerSeries.order_mul {R : Type u_1} [CommRing R] [IsDomain R] (φ : PowerSeries R) (ψ : PowerSeries R) :
      (φ * ψ).order = φ.order + ψ.order

      The order of the product of two formal power series over an integral domain is the sum of their orders.