LeanPool.VirasoroProject.ToMathlib.LinearAlgebra.Basis.Defs #
noncomputable def
Finsupp.basisFun
(X : Type u_1)
(R : Type u_2)
[Semiring R]
:
Module.Basis X R (X →₀ R)
Standard basis of the space of finitely supported functions.
Equations
- Finsupp.basisFun X R = { repr := LinearEquiv.refl R (X →₀ R) }