basis of free module `X -> R` with [fintype X]?

Stream: Is there code for X?

[Kevin Buzzard]

@orlando was asking me about the standard basis for finite free modules. All the std_basis machinery seems to be set up for arbitrary products (where the standard basis is not a basis). Where should he look for facts about the free $R$-module $R^n$?

[Johan Commelin]

Is there nothing about this in linear_algebra/basis.lean?

[Kevin Buzzard]

There is stuff like equiv_fun_basis there Orlando -- is this enough for you?

[orlando]

hum i see also is_basis_fun ! in linear_algebra/ basis