English
The exponential function provides a monoid homomorphism from the multiplicative complex numbers to the complex numbers; i.e., it respects multiplication and sends 1 to 1.
Русский
Экспонента определяет моноид-гомоморфизм от мультипликативного множества комплексных чисел к комплексным числам; то есть сохраняет умножение и отправляет 1 в 1.
LaTeX
$$$\\text{expMonoidHom} : \\mathrm{MonoidHom}(\\mathrm{Multiplicative}\\ \\mathbb{C}, \\mathbb{C})$, с $(\\mathrm{toFun}(z) = \\exp(z))$, \\text{ и } \\text{map\_mul}'(a,b) = \\exp(a)\\exp(b)$$$
Lean4
@[simp]
theorem exp_zero : exp 0 = 1 := by
rw [exp]
refine lim_eq_of_equiv_const fun ε ε0 => ⟨1, fun j hj => ?_⟩
convert (config := .unfoldSameFun) ε0
rcases j with - | j
· exact absurd hj (not_le_of_gt zero_lt_one)
· dsimp [exp']
induction j with
| zero => simp
| succ j ih =>
rw [← ih (by simp)]
simp only [sum_range_succ, pow_succ]
simp
