Divisibility of power series by constants

A constant power series C r divides f exactly when r divides every coefficient of f. This is the power-series form of Mathlib's Polynomial.C_dvd_iff_dvd_coeff and MvPolynomial.C_dvd_iff_dvd_coeff, and the one-variable case of MvPowerSeries.C_dvd_iff_dvd_coeff.

It is the step that removes a common power of a uniformiser from the coefficients of a power series over a discrete valuation ring before applying Weierstrass preparation.

Main results

• PowerSeries.C_dvd_iff_dvd_coeff: C r ∣ f ↔ ∀ n, r ∣ coeff n f.

theorem PowerSeries.C_dvd_iff_dvd_coeff {R : Type u_1} [Semiring R] (r : R) (f : PowerSeries R) : C r ∣ f ↔ ∀ (n : ℕ), r ∣ (coeff n) f

A constant power series C r divides f if and only if r divides every coefficient of f.