English
The Bernoulli' power series multiplied by (exp − 1) equals X times exp, i.e., Bernoulli'PowerSeries · (exp − 1) = X · exp.
Русский
Умножение ряда Бернулли' на (exp − 1) даёт X · exp.
LaTeX
$$$\text{bernoulli'PowerSeries } A \; * (\exp A - 1) = X \; * \exp A$$$
Lean4
theorem bernoulli'PowerSeries_mul_exp_sub_one : bernoulli'PowerSeries A * (exp A - 1) = X * exp A :=
by
ext n
cases n with
| zero => simp
| succ n =>
rw [bernoulli'PowerSeries, coeff_mul, mul_comm X, sum_antidiagonal_succ']
suffices (∑ p ∈ antidiagonal n, bernoulli' p.1 / p.1! * ((p.2 + 1) * p.2! : ℚ)⁻¹) = (n ! : ℚ)⁻¹ by
simpa [map_sum, Nat.factorial] using congr_arg (algebraMap ℚ A) this
apply eq_inv_of_mul_eq_one_left
rw [sum_mul]
convert bernoulli'_spec' n using 1
apply sum_congr rfl
simp_rw [mem_antidiagonal]
rintro ⟨i, j⟩ rfl
have := factorial_mul_factorial_dvd_factorial_add i j
simp [field, add_choose, *]
