[Merged by Bors] - fix: redefine semiring instance on tensor product#6141
[Merged by Bors] - fix: redefine semiring instance on tensor product#6141eric-wieser wants to merge 8 commits intomasterfrom
Conversation
|
!bench |
| left_distrib a b c := show mul a (b + c) = mul a b + mul a c by simp | ||
| right_distrib a b c := show mul (a + b) c = mul a c + mul b c by simp | ||
| zero_mul a := show mul 0 a = 0 by simp | ||
| mul_zero a := show mul a 0 = 0 by simp |
There was a problem hiding this comment.
Are we missing simp lemmas or something? Why might this have stopped working? Note that the type of mul is LinearMap rather than just a function. Note also that this was already an issue on master.
There was a problem hiding this comment.
This stopped working because these fields are about HMul.hMul, but the mul field we provide is Mul.mul. The goals can be solved with simp [HMul.hMul]. This probably comes up all over the place when building structures, and the answer is always going to be "you have to unfold HFoo.foo too".
|
!bench |
|
Here are the benchmark results for commit a022cfe. |
|
Here are the benchmark results for commit cbfe65e. Benchmark Metric Change
====================================================================
+ ~Mathlib.Algebra.Category.Ring.Constructions instructions -12.6%
+ ~Mathlib.Data.Matrix.Kronecker instructions -22.4%
+ ~Mathlib.RingTheory.Etale instructions -9.7%
+ ~Mathlib.RingTheory.IntegralClosure instructions -8.2%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -24.0%
+ ~Mathlib.RingTheory.Kaehler instructions -45.0%
+ ~Mathlib.RingTheory.RingHom.Finite instructions -31.8%
+ ~Mathlib.RingTheory.RingHom.Integral instructions -47.1%
+ ~Mathlib.RingTheory.RingHom.Surjective instructions -7.2%
+ ~Mathlib.RingTheory.RingHomProperties instructions -20.6%
+ ~Mathlib.RingTheory.TensorProduct instructions -14.8% |
a157f02 to
d1db49f
Compare
|
This is much better, thanks! bors d+ |
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
By providing the `Mul` instance up front, this seems to make future typeclass search much easier. This comes at the expense of causing minor elaboration problem in various tensor definitions, which now require the implicit type arguments to be provided explicitly. This also simplifies some proofs, removing a porting note. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
In light of #6141, we can change the heart beats to more representantive numbers. Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
In light of #6141, we can change the heart beats to more representantive numbers. Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
By providing the `Mul` instance up front, this seems to make future typeclass search much easier. This comes at the expense of causing minor elaboration problem in various tensor definitions, which now require the implicit type arguments to be provided explicitly. This also simplifies some proofs, removing a porting note. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
In light of #6141, we can change the heart beats to more representantive numbers. Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
By providing the
Mulinstance up front, this seems to make future typeclass search much easier.This comes at the expense of causing minor elaboration problem in various tensor definitions, which now require the implicit type arguments to be provided explicitly.
This also simplifies some proofs, removing a porting note.
This is a test to try and work out what's going on in #6134.
This skips out some intermediate instances to try and answer the question of whether they matter.