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.min_order_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
.
The 0
power series is the unique power series with infinite order.
If the order of a formal power series is finite, then the coefficient indexed by the order is nonzero.
If the n
th coefficient of a formal power series is nonzero,
then the order of the power series is less than or equal to n
.
The n
th coefficient of a formal power series is 0
if n
is strictly
smaller than the order of the power series.
The order of a formal power series is at least n
if
the i
th coefficient is 0
for all i < n
.
The order of a formal power series is exactly n
if the n
th coefficient is nonzero,
and the i
th coefficient is 0
for all i < n
.
Alias of PowerSeries.min_order_le_order_add
.
The order of the sum of two formal power series is at least the minimum of their orders.
Alias of PowerSeries.le_order_mul
.
The order of the product of two formal power series is at least the sum of their orders.
Given a non-zero power series f
, divXPowOrder f
is the power series obtained by
dividing out the largest power of X that divides f
, that is its order
Equations
- f.divXPowOrder = PowerSeries.mk fun (n : ℕ) => (PowerSeries.coeff R (n + f.order.toNat)) f
Instances For
Alias of PowerSeries.divXPowOrder
.
Given a non-zero power series f
, divXPowOrder f
is the power series obtained by
dividing out the largest power of X that divides f
, that is its order
Instances For
Alias of PowerSeries.X_pow_order_mul_divXPowOrder
.
The order of the formal power series 1
is 0
.
The order of an invertible power series is 0
.
The order of the formal power series X
is 1
.
The order of the formal power series X^n
is n
.
Dividing X
by the maximal power of X
dividing it leaves 1
.
Alias of PowerSeries.divXPowOrder_X
.
Dividing X
by the maximal power of X
dividing it leaves 1
.
The order of the product of two formal power series over an integral domain is the sum of their orders.
The operation of dividing a power series by the largest possible power of X
preserves multiplication.
Alias of PowerSeries.divXPowOrder_mul_divXPowOrder
.
The operation of dividing a power series by the largest possible power of X
preserves multiplication.