English
The map sending a solution to its first E.order terms is a linear equivalence between the solution space and Fin E.order → R.
Русский
Отображение, отправляющее решение в его первые E.order членов, является линейным эквидом между пространством решений и Fin E.order → R.
LaTeX
$$toInit : E.solSpace ≃ₗ[R] Fin E.order → R$$
Lean4
/-- The function that maps a solution `u` of `E` to its first
`E.order` terms as a `LinearEquiv`. -/
def toInit : E.solSpace ≃ₗ[R] Fin E.order → R
where
toFun u x := (u : ℕ → R) x
map_add' u
v := by
ext
simp
map_smul' a
u := by
ext
simp
invFun u := ⟨E.mkSol u, E.is_sol_mkSol u⟩
left_inv u := by ext n; symm; apply E.eq_mk_of_is_sol_of_eq_init u.2; intro k; rfl
right_inv u := funext_iff.mpr fun n ↦ E.mkSol_eq_init u n
