Stream: Is there code for X?
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
linear_algebra/basic.lean, but I can't figure out how to use it.
Kenny Lau (Jul 24 2020 at 20:39):
Markus Himmel (Jul 24 2020 at 20:45):
Last updated: May 17 2021 at 16:26 UTC