PowerSeries.sub_const_eq_shift_mul_X

theorem PowerSeries.sub_const_eq_shift_mul_X : ∀ {R : Type u_1} [inst : Ring R] (φ : PowerSeries R), φ - (PowerSeries.C R) ((PowerSeries.constantCoeff R) φ) = (PowerSeries.mk fun p => (PowerSeries.coeff R (p + 1)) φ) * PowerSeries.X

This theorem states that for any formal power series `φ` over a ring `R`, subtracting the constant coefficient of `φ` from `φ` itself is equivalent to shifting the coefficients of `φ` by one place to the right and multiplying the result by the formal power series variable `X`. In other words, if we denote the `n`th coefficient of `φ` by `φ[n]`, the power series obtained by replacing `φ[n]` with `φ[n+1]` for all `n` and multiplying by `X` is the same as the power series obtained by subtracting the constant term `φ[0]` from `φ`.

More concisely: For any formal power series `φ` over a ring `R`, `φ - φ[0]` is equivalent to shifting the coefficients of `φ` by one place to the right and multiplying the result by the formal power series variable `X`.