English
The standard basis of the endomorphism algebra End_R(M) is the basis End_R(M) indexed by pairs (i, j) giving the map sending basis vector j to i and others to zero.
Русский
Стандартная база алгебры эндоморфизмов End_R(M) задаётся парами (i, j) и отображает b_j в b_i, а остальные базисные вектора в 0.
LaTeX
$$$\\text{end}(b) = b.linearMap b$$$
Lean4
/-- The standard basis of the endomorphism algebra of a module
induced by a basis of the module.
If `M` is a module with basis `b` indexed by a finite type `ι`,
then `Basis.end b` is the basis of `Module.End R M` indexed by `ι × ι`
where `(i, j)` indexes the linear map that sends `b j` to `b i`
and sends all other basis vectors to `0`. -/
@[simps! -isSimp repr_apply repr_symm_apply]
noncomputable abbrev «end» (b : Basis ι R M) : Basis (ι × ι) R (Module.End R M) :=
b.linearMap b
