English
Let x be an element of the trivial square-zero extension tsze R M. For every natural number n, the first component of the exponential series on tsze R M equals the exponential series of the first component on R: fst(expSeries 𝕜 (tsze R M) n (λ _ => x)) = expSeries 𝕜 R n (λ _ => x.fst).
Русский
Пусть x принадлежит тривиальному разложения квадрата нулей tsze R M. Для любого натурального числа n первая координата экспоненциального ряда на tsze R M равна экспоненциальному ряду по первой координате на R: fst(expSeries 𝕜 (tsze R M) n (λ _ => x)) = expSeries 𝕜 R n (λ _ => x.fst).
LaTeX
$$$$\\ fst\\big(\\expSeries 𝕜 (tsze R M)\\, n\\, (\\lambda\\_ => x)\\big) \\,=\, \\expSeries 𝕜 R\\, n\\, (\\lambda\\_ => x.fst) $$$$
Lean4
@[simp]
theorem fst_expSeries (x : tsze R M) (n : ℕ) :
fst (expSeries 𝕜 (tsze R M) n fun _ => x) = expSeries 𝕜 R n fun _ => x.fst := by simp [expSeries_apply_eq]
