[Merged by Bors] - feat(LinearAlgebra/TensorProduct): add TensorProduct.map₂
#10986
Conversation
jjaassoonn
commented
Feb 26, 2024
jjaassoonn
commented
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
jjaassoonn
changed the title
TensorProduct.map2TensorProduct.map₂
jjaassoonn
added
awaiting-review
|
Thanks! bors d+ |
|
✌️ jjaassoonn can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
and removed
awaiting-review
|
Can you use this to golf the |
done |
|
Once you've added the docstring, please run a benchmark (it will fail at the moment because the missing docstring will cause a linter error) |
|
!bench |
|
Here are the benchmark results for commit ef495da. Benchmark Metric Change
===================================================
- ~Mathlib.RingTheory.Kaehler instructions 5.8% |
|
How do we feel about the benchmark result. Is the slow down statistically insignificant? |
|
bors merge |
|
I think it's ok; I tried golfing this a long time ago in #6195 and got a timeout; 5% is a much less bad outcome! |
| -/ | ||
| def mulAux (a₁ : A) (b₁ : B) : A ⊗[R] B →ₗ[R] A ⊗[R] B := | ||
| TensorProduct.map (LinearMap.mulLeft R a₁) (LinearMap.mulLeft R b₁) | ||
| #align algebra.tensor_product.mul_aux Algebra.TensorProduct.mulAux |
There was a problem hiding this comment.
These should be noaligned
bors r-
bors d+
There was a problem hiding this comment.
do you mean I should keep these code but just noalign them? Note that I have added
#noalign algebra.tensor_product.mul_aux
#noalign algebra.tensor_product.mul_aux_apply
|
✌️ jjaassoonn can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Canceled. |
leanprover-community-mathlib4-bot
added
the
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
TensorProduct.map₂TensorProduct.map₂
