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): move is_basis_std_basis
to std_basis.lean
#6054
Conversation
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.
src/linear_algebra/std_basis.lean
Outdated
|
||
## Main definitions | ||
|
||
- `std_basis R ϕ i b`: the `i`'th standard `R`-basis vector on `Π i, ϕ i` |
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.
Perhaps add "scaled by b"?
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.
It's not exactly scaled since φ
is just a semimodule. I'll use that for now unless someone has a nice alternative.
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.
Oh, I see your point - the semimodule may not have a 1
.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
bors d+ |
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
I'll let @eric-wieser look for one more style suggestion, then I will merge :) |
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.
No more comments from me :)
bors r+ |
…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>
Pull request successfully merged into master. Build succeeded: |
is_basis_std_basis
to std_basis.lean
is_basis_std_basis
to std_basis.lean
…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>
This is a follow-up to #6020 which moved
std_basis
to a new file: now move results frombasis.lean
to that same file.CC @eric-wieser