English
Let x ∈ tsze R M and suppose the commutation hx = MulOpposite.op x.fst • x.snd = x.fst • x.snd holds. Then for every n, the second (snd) component of the exponential series on the extension satisfies snd(expSeries 𝕜 (tsze R M) (n + 1) (λ _ => x)) = (expSeries 𝕜 R n (λ _ => x.fst)) • x.snd.
Русский
Пусть x ∈ tsze R M и выполняется условие непротиворечивости hx = MulOpposite.op x.fst • x.snd = x.fst • x.snd. Тогда для любого n вторая (snd) компонента экспоненциального ряда над расширением удовлетворяет snd(expSeries 𝕜 (tsze R M) (n + 1) (λ _ => x)) = (expSeries 𝕜 R n (λ _ => x.fst)) • x.snd.
LaTeX
$$$$ snd\\big(\\expSeries 𝕜 (tsze R M) (n + 1) (\\lambda _ => x)\\big) = \\Big(\\expSeries 𝕜 R n (\\lambda _ => x.fst)\\Big) \\cdot x.snd $$$$
Lean4
theorem snd_expSeries_of_smul_comm (x : tsze R M) (hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd) (n : ℕ) :
snd (expSeries 𝕜 (tsze R M) (n + 1) fun _ => x) = (expSeries 𝕜 R n fun _ => x.fst) • x.snd := by
simp_rw [expSeries_apply_eq, snd_smul, snd_pow_of_smul_comm _ _ hx, ← Nat.cast_smul_eq_nsmul 𝕜 (n + 1), smul_smul,
smul_assoc, Nat.factorial_succ, Nat.pred_succ, Nat.cast_mul, mul_inv_rev,
inv_mul_cancel_right₀ ((Nat.cast_ne_zero (R := 𝕜)).mpr <| Nat.succ_ne_zero n)]
