New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(linear_algebra/std_basis): move std_basis to a new file #6020
Conversation
linear_algebra/basic is _very_ long. This reduces its length by about 5%. Authorship of the std_basis stuff seems to come almost entirely from 10a586b. None of the lemmas have changed, and the variables are kept in exactly the same order as before.
4ffd786
to
052d523
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I love refactors of linear_algebra
❤️
Should we take the opportunity to shorten basis.lean
as well, moving some std_basis
results to the new std_basis
file?
elsewhere. | ||
|
||
To give a concrete example, `std_basis R (λ (i : fin 3), R) i 1` gives the `i`th unit basis vector | ||
in `R³`, and `pi.is_basis_fun` proves this is a basis over `fin 3 → R`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Since this file doesn't actually prove that the standard basis is a basis, maybe the import hierarchy should go basic.lean
-> basis.lean
-> std_basis.lean
?
Moving the is_basis statements is probably a good idea, but since I don't plan to come back to this today my preference would be just to merge it so that the build time is slightly shorter (not incurring |
Sounds good. Maybe I'll look into moving the bors r+ |
linear_algebra/basic is _very_ long. This reduces its length by about 5%. Authorship of the std_basis stuff seems to come almost entirely from 10a586b. None of the lemmas have changed, and the variables are kept in exactly the same order as before.
Pull request successfully merged into master. Build succeeded: |
This is a follow-up to #6020 which moved `std_basis` to a new file, now we move results about `std_basis` to that same file.
…6054) This is a follow-up to #6020 which moved `std_basis` to a new file: now move results from `basis.lean` to that same file. CC @eric-wieser Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
linear_algebra/basic is _very_ long. This reduces its length by about 5%. Authorship of the std_basis stuff seems to come almost entirely from 10a586b. None of the lemmas have changed, and the variables are kept in exactly the same order as before.
…6054) This is a follow-up to #6020 which moved `std_basis` to a new file: now move results from `basis.lean` to that same file. CC @eric-wieser Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
linear_algebra/basic is very long. This reduces its length by about 5%.
Authorship of the std_basis stuff seems to come almost entirely from 10a586b.
None of the lemmas have changed, and the variables are kept in exactly the same order as before.