English
For x ∈ tsze R M with hx = MulOpposite.op x.fst • x.snd = x.fst • x.snd, the exponential of x in tsze R M decomposes as exp 𝕜 x = inl (exp 𝕜 x.fst) + inr (exp 𝕜 x.fst • x.snd).
Русский
Пусть x имеет разложение x = inl x.fst + inr x.snd в тривиальном квадратном дополнении; тогда экспонента от x равна сумма экспоненты по первой координате и экспоненты по первой координате, умноженной на вторую координату.
LaTeX
$$$$ \\exp 𝕜 x = inl(\\exp 𝕜 x.fst) + inr(\\exp 𝕜 x.fst \\cdot x.snd) $$$$
Lean4
theorem exp_def_of_smul_comm (x : tsze R M) (hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd) :
exp 𝕜 x = inl (exp 𝕜 x.fst) + inr (exp 𝕜 x.fst • x.snd) :=
by
simp_rw [exp, FormalMultilinearSeries.sum]
by_cases h : Summable (fun (n : ℕ) => (expSeries 𝕜 R n) fun _ ↦ fst x)
· refine (hasSum_expSeries_of_smul_comm 𝕜 x hx ?_).tsum_eq
exact h.hasSum
· rw [tsum_eq_zero_of_not_summable h, zero_smul, inr_zero, inl_zero, zero_add, tsum_eq_zero_of_not_summable]
simp_rw [← fst_expSeries] at h
refine mt ?_ h
exact (Summable.map · (TrivSqZeroExt.fstHom 𝕜 R M).toLinearMap continuous_fst)
