Power series whose coefficients multiply like divided powers

A sequence (γₙ) in a commutative semiring multiplies like divided powers when γₘ * γₙ = (m + n).choose m • γₘ₊ₙ for all m and n; these are the multiplication relations of a divided power structure, and the coefficients of exp(a X) = ∑ (aⁿ / n!) Xⁿ satisfy them over a ℚ-algebra. This file proves that the power series whose coefficients multiply like divided powers are closed under multiplication. The proof is the Vandermonde identity Nat.add_choose_eq, and divides by no factorial.

This closure is what makes the divided-power exponential ∑ₙ γₙ(x) Xⁿ of a sum of elements satisfy the multiplication relations again, as in the base change of divided power algebras.

Main declarations

• PowerSeries.coeff_mul_coeff_mul_eq_choose_nsmul: if the coefficients of f and of g multiply like divided powers, then so do those of f * g.

theorem PowerSeries.coeff_mul_coeff_mul_eq_choose_nsmul {A : Type u_1} [CommSemiring A] {f g : PowerSeries A} (hf : ∀ (m n : ℕ), (coeff m) f * (coeff n) f = (m + n).choose m • (coeff (m + n)) f) (hg : ∀ (m n : ℕ), (coeff m) g * (coeff n) g = (m + n).choose m • (coeff (m + n)) g) (m n : ℕ) : (coeff m) (f * g) * (coeff n) (f * g) = (m + n).choose m • (coeff (m + n)) (f * g)

If the coefficients of f and of g multiply like divided powers, that is fₘ * fₙ = (m + n).choose m • fₘ₊ₙ and likewise for g, then so do the coefficients of f * g.