Zulip Chat Archive

Stream: Is there code for X?

Topic: std_basis


view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jul 24 2020 at 20:39):

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

view this post on Zulip Markus Himmel (Jul 24 2020 at 20:45):

Perfect, thanks!


Last updated: May 17 2021 at 16:26 UTC