English
The identity e^{aX} e^{bX} = e^{(a+b)X} holds in the power series ring, reflecting the additivity of exponents.
Русский
Имеется тождество экспоненты: e^{aX} e^{bX} = e^{(a+b)X} в кольце степенных рядов.
LaTeX
$$$$ e^{aX} e^{bX} = e^{(a+b)X} $$$$
Lean4
/-- Shows that $e^{aX} * e^{bX} = e^{(a + b)X}$ -/
theorem exp_mul_exp_eq_exp_add [Algebra ℚ A] (a b : A) :
rescale a (exp A) * rescale b (exp A) = rescale (a + b) (exp A) :=
by
ext n
simp only [coeff_mul, exp, rescale, coeff_mk, MonoidHom.coe_mk, OneHom.coe_mk, coe_mk,
Nat.sum_antidiagonal_eq_sum_range_succ_mk, add_pow, sum_mul]
apply sum_congr rfl
rintro x hx
suffices
a ^ x * b ^ (n - x) * (algebraMap ℚ A (1 / ↑x.factorial) * algebraMap ℚ A (1 / ↑(n - x).factorial)) =
a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n.factorial))
by convert this using 1 <;> ring
congr 1
rw [← map_natCast (algebraMap ℚ A) (n.choose x), ← map_mul, ← map_mul]
refine RingHom.congr_arg _ ?_
rw [mul_one_div (↑(n.choose x) : ℚ), one_div_mul_one_div]
symm
rw [div_eq_iff, div_mul_eq_mul_div, one_mul, choose_eq_factorial_div_factorial]
· norm_cast
rw [cast_div_charZero]
apply factorial_mul_factorial_dvd_factorial (mem_range_succ_iff.1 hx)
· apply mem_range_succ_iff.1 hx
· rintro h
apply factorial_ne_zero n
rw [cast_eq_zero.1 h]
