English
General version: the formal power series product identity for exponentials holds for any DividedPowers I: exp_add', linking dpow with products of dpow.
Русский
Общее утверждение: тождество в производных степенях множителя соответствует умножению степенных рядов экспоненты, через dpow.
LaTeX
$$$$ \\mathrm{exp\_add} \\; (hI) \\; (ha) (hb) : \\; \\mathrm{PowerSeries.mk}(n \\mapsto hI.dpow n(a+b)) = \\mathrm{PowerSeries.mk}(n \\mapsto hI.dpow n a) \\cdot \\mathrm{PowerSeries.mk}(n \\mapsto hI.dpow n b) $$$$
Lean4
/-- A more general of `DividedPowers.exp_add` -/
theorem exp_add' (dp : ℕ → A → A) (dp_add : ∀ n, dp n (a + b) = (antidiagonal n).sum fun k ↦ dp k.1 a * dp k.2 b) :
PowerSeries.mk (fun n ↦ dp n (a + b)) = (PowerSeries.mk fun n ↦ dp n a) * (PowerSeries.mk fun n ↦ dp n b) :=
by
ext n
simp only [PowerSeries.coeff_mk, PowerSeries.coeff_mul, dp_add n, sum_antidiagonal_eq_sum_range_succ_mk]
