English
Let b be a basis of M. The map that sends a functional l ∈ Dual R M to the function i ↦ l(b_i) is injective; equivalently, if l and l′ agree on every basis vector, then l = l′.
Русский
Пусть база b в M. Отображение l ↦ (i ↦ l(b_i)) из пространства двойств к набору координат инъективно; то есть если два функционала совпадают на всех базисных векторах, то они равны.
LaTeX
$$$ \\text{Dual.eval } R M : \\mathrm{Dual}R M \\to ι \\to R \\quad \\text{ is injective, i.e. } (\\forall l,l'\\in \\mathrm{Dual}R M)(\\forall i\\, l(b_i)=l'(b_i)\\Rightarrow l=l'). $$$
Lean4
theorem eval_injective {ι : Type*} (b : Basis ι R M) : Function.Injective (Dual.eval R M) :=
by
intro m m' eq
simp_rw [LinearMap.ext_iff, Dual.eval_apply] at eq
exact b.ext_elem fun i ↦ eq (b.coord i)
