English
For a basis b, the i-th vector is obtained by applying the inverse of the basis isomorphism to the unit coordinate at i; that is, b_i = repr_b^{-1}(δ_i) where δ_i is the unit vector with 1 at i and 0 elsewhere.
Русский
Пусть b — базис. i-ый вектор получается как обратное образBasis-изоморфизма применимое к единичному вектору δ_i, то есть b_i = repr_b^{-1}(δ_i), где δ_i имеет 1 на координате i и 0 в остальных местах.
LaTeX
$$$b_i = \mathrm{repr}_b^{-1}(\delta_i) = (\mathrm{repr}_b)^{-1}(\mathrm{Finsupp}.single\ i\ 1)$$$
Lean4
/-- `b i` is the `i`th basis vector. -/
instance instFunLike : FunLike (Basis ι R M) ι M
where
coe b i := b.repr.symm (Finsupp.single i 1)
coe_injective' f g
h :=
repr_injective <|
LinearEquiv.symm_bijective.injective <| LinearEquiv.toLinearMap_injective <| by ext; exact congr_fun h _
