## Stream: Is there code for X?

### Topic: std_basis

#### Markus Himmel (Jul 24 2020 at 20:26):

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 (Jul 24 2020 at 20:39):

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

#### Markus Himmel (Jul 24 2020 at 20:45):

Perfect, thanks!

Last updated: May 17 2021 at 16:26 UTC