-
Notifications
You must be signed in to change notification settings - Fork 298
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] - refactor(data/matrix/basic): merge duplicate algebra structures #8486
Conversation
06cd890
to
68c2784
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 never noticed the duplicate algebra
s, thanks for spotting it!
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
bors d+ |
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
Canceled. |
628cd0e
to
7ec6d40
Compare
bors r+ |
By putting the algebra instance in the same file as `scalar`, a future patch can probably remove `matrix.scalar` entirely (it's just another spelling of `algebra_map`). Note that we actually had two instances of `algebra R (matrix n n R)` in different files, and the second one was strictly more general than the first. This removes the less general one. Moving the imports around like this changes the number of simp lemmas available in downstream files, which can make `simp` slow enough to push a proof into a timeout. A lot of files were expecting a transitive import of `algebra.algebra.basic` to import `data.fintype.card`, which it no longer does; hence the need to add this import explicitly. There are no new lemmas or generalizations in this change; the old `matrix_algebra` has been deleted, and everything else has been moved with some variables renamed.
Pull request successfully merged into master. Build succeeded: |
By putting the algebra instance in the same file as
scalar
, a future patch can probably removematrix.scalar
entirely (it's just another spelling ofalgebra_map
).Note that we actually had two instances of
algebra R (matrix n n R)
in different files, and the second one was strictly more general than the first. This removes the less general one.Moving the imports around like this changes the number of simp lemmas available in downstream files, which can make
simp
slow enough to push a proof into a timeout.A lot of files were expecting a transitive import of
algebra.algebra.basic
to importdata.fintype.card
, which it no longer does; hence the need to add this import explicitly.There are no new lemmas or generalizations in this change; the old
matrix_algebra
has been deleted, and everything else has been moved with some variables renamed.