English
The range of the evaluation map Dual.eval R M is the whole target space; i.e., range(Dual.eval R M) = ⊤.
Русский
Образ отображения оценки Dual.eval R M равен всей цели; то есть range(Dual.eval R M) = ⊤.
LaTeX
$$$ \\mathrm{range}(\\mathrm{Dual.eval} \\; R\\; M) = \\top $$$
Lean4
theorem eval_range {ι : Type*} [Finite ι] (b : Basis ι R M) : LinearMap.range (Dual.eval R M) = ⊤ := by
classical
cases nonempty_fintype ι
rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]