[Merged by Bors] - feat: make multiplication in [Add]MonoidAlgebra irreducible #12554
Conversation
fpvandoorn
added
awaiting-review
| @@ -162,16 +162,18 @@ section Mul | |||
|
|
|||
| variable [Semiring k] [Mul G] | |||
|
|
|||
| irreducible_def mul' (f g : MonoidAlgebra k G) : MonoidAlgebra k G := | |||
There was a problem hiding this comment.
Do we get the same benefits with just @[irreducible]?
There was a problem hiding this comment.
I didn't check. Are there advantages of @[irreducible]?
There was a problem hiding this comment.
Yeah you get the same benefits in terms of the speed-up.
The auto-*_def declarations are convenient but you can force things with with_unfolding_all if necessary.
I would generally prefer to depend on upstream tooling unless we absolutely need something that can/will not be provided. But I don't feel strongly enough to put up a fight.
There was a problem hiding this comment.
Those are good points.
We get the same improvement, with @[irreducible], so I modified this PR.
There was a problem hiding this comment.
Using the @[irreducible] is there a way to "unfold irreducible definition X, but no other irreducible definitions"? I tried simp [mul'] or unfold mul', but they both seem to fail.
There was a problem hiding this comment.
I don't know of a way to that unfortunately.
There was a problem hiding this comment.
We also used private for Real.
There was a problem hiding this comment.
That is orthogonal to irreducibility, and I don't particularly care about making this private.
There was a problem hiding this comment.
I would like to have a consistent design across the library, or there is a reason why the design is different. But I would not insist.
There was a problem hiding this comment.
Better to do things like this (improving consistency) in separate PRs, rather than bundling it in because the relevant file was touched.
|
!bench |
|
Here are the benchmark results for commit c6fd2d1. |
|
bors merge |
github-actions
bot
added
ready-to-merge
* See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/multiplication.20on.20MvPolynomial.20should.20be.20irreducible) * The example in that thread takes ~55000ms on master and 43ms on this branch. * I expect that this will lead to little gains in the (working) proofs of Mathlib. * The multiplication on `MonoidAlgebra _ G` and `AddMonoidAlgebra _ (Additive G)` are still defeq the same.
|
Build failed (retrying...): |
* See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/multiplication.20on.20MvPolynomial.20should.20be.20irreducible) * The example in that thread takes ~55000ms on master and 43ms on this branch. * I expect that this will lead to little gains in the (working) proofs of Mathlib. * The multiplication on `MonoidAlgebra _ G` and `AddMonoidAlgebra _ (Additive G)` are still defeq the same.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
* See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/multiplication.20on.20MvPolynomial.20should.20be.20irreducible) * The example in that thread takes ~55000ms on master and 43ms on this branch. * I expect that this will lead to little gains in the (working) proofs of Mathlib. * The multiplication on `MonoidAlgebra _ G` and `AddMonoidAlgebra _ (Additive G)` are still defeq the same.
* See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/multiplication.20on.20MvPolynomial.20should.20be.20irreducible) * The example in that thread takes ~55000ms on master and 43ms on this branch. * I expect that this will lead to little gains in the (working) proofs of Mathlib. * The multiplication on `MonoidAlgebra _ G` and `AddMonoidAlgebra _ (Additive G)` are still defeq the same.
MonoidAlgebra _ GandAddMonoidAlgebra _ (Additive G)are still defeq the same.