std_basis

Stream: Is there code for X?

[Markus Himmel]

At LFTCM, there was an exercise to show that

def std_basis (i : n) : (n → R) := λ j, if i = j then 1 else 0

is a basis. Is this result in mathlib? I know there's something called std_basis in linear_algebra/basic.lean, but I can't figure out how to use it.

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/4d81149366b4b88fe72784f08a906c613af85a13/src/linear_algebra/basis.lean#L1289

[Markus Himmel]

Perfect, thanks!