Divisibility of multivariate power series by constants

A constant power series C r divides f exactly when r divides every coefficient of f. This is the multivariate form of PowerSeries.C_dvd_iff_dvd_coeff, and the power-series form of Mathlib's MvPolynomial.C_dvd_iff_dvd_coeff; the quotient is assembled from the infinitely many coefficient quotients at once.

It turns a congruence of power series that holds coefficientwise modulo r, for instance one proved after reducing the coefficients modulo r, into divisibility in the power series ring, where it can be raised to powers.

Main results

• MvPowerSeries.C_dvd_iff_dvd_coeff: C r ∣ f ↔ ∀ d, r ∣ coeff d f.

theorem MvPowerSeries.C_dvd_iff_dvd_coeff {σ : Type u_1} {R : Type u_2} [Semiring R] (r : R) (f : MvPowerSeries σ R) : C r ∣ f ↔ ∀ (d : σ →₀ ℕ), r ∣ (coeff d) f

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