[Merged by Bors] - refactor(LinearAlgebra/Matrix/SesquilinearForm): Sesquilinear Maps and Matrices#9334
[Merged by Bors] - refactor(LinearAlgebra/Matrix/SesquilinearForm): Sesquilinear Maps and Matrices#9334
Conversation
…inearMaps-Matrix1
|
!bench |
|
Here are the benchmark results for commit 1ad926c. Benchmark Metric Change
======================================================================
- ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm instructions 6.1% |
|
!bench |
|
Here are the benchmark results for commit 6f6a726. Benchmark Metric Change
======================================================================
- ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm instructions 31.4% |
|
@j-loreaux unfortunately the benchmarks look slightly worse (I'm assuming a larger percentage in red is worse?) |
|
That's such a small change, and only in a single file, that it's not a big deal. It could even be noise. |
|
General information: 7 files got slower by at least 10⁹ instructions: 2 files got slower by at least 10%: No file got faster by at least 10⁹ instructions. No file got faster by at least 10%. |
|
Thanks @MichaelStollBayreuth I'll let someone else decide. But I'm okay with this. The other option would be to have these general versions, and then more specific ones which are maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by j-loreaux. |
Vierkantor
left a comment
There was a problem hiding this comment.
I found a few stylistic issues. Overall I think the slower build time is worth it for the increased generality.
So looks good to me with these changes, thanks!
bors d+
|
✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
bors r+ |
…d Matrices (#9334) Some of the concepts in `LinearAlgebra/Matrix/SesquilinearForm` can be generalised from Sesquilinear Forms to Sesquilinear Maps with little or no impact on the rest of Mathlib. This PR makes those generalisations. A number of results in the `ToMatrix` section relating composition of maps to matrix multiplication could also be generalised, but they require a more genralised notion of matrix multiplication than we currently have available, so they are not included in the scope of this PR. Similarly for most of the results in the `Det` section. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>
|
Pull request successfully merged into master. Build succeeded: |
Some of the concepts in
LinearAlgebra/Matrix/SesquilinearFormcan be generalised from Sesquilinear Forms to Sesquilinear Maps with little or no impact on the rest of Mathlib. This PR makes those generalisations.A number of results in the
ToMatrixsection relating composition of maps to matrix multiplication could also be generalised, but they require a more genralised notion of matrix multiplication than we currently have available, so they are not included in the scope of this PR. Similarly for most of the results in theDetsection.See also: #9312
Hopefully this will replace #8256, in part at least.