[Merged by Bors] - refactor(Algebra/Star/*): Allow for star operation on non-associative algebras #6562
Conversation
|
!bench |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
mans0954
added
the
awaiting-review
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
I was hoping the benchmark bot would respond; maybe it crashed? !bench |
|
!bench |
|
!bench |
|
Here are the benchmark results for commit 6afc5de.Found no runs to compare against. |
…/non-assoc-star-mul
|
I've merged in a commit from master that I know has a benchmark, in the hope that it produces a comparison. |
|
!bench |
|
Here are the benchmark results for commit 1362a3a. Benchmark Metric Change
=========================================================================
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint instructions -5.3%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality instructions -8.0%
- ~Mathlib.Analysis.VonNeumannAlgebra.Basic instructions 17.3% |
|
@eric-wieser do we need to do something as a result of the benchmarks? |
|
No, I think it's probably fine; I just wanted to check it didn't majorly slow down every file about star operations. I'll let @j-loreaux give the final review on this, |
|
bors d+ |
|
✌️ mans0954 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
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
|
bors r+ |
… algebras (#6562) Typically a * operation on a mathematical structure `R` equipped with a multiplication is an involutive anti-automorphism i.e. ``` ∀ r s : R, star (r * s) = star s * star r ``` Currently mathlib defines a class `StarSemigroup` to be a semigroup satisfying this property. However, the requirement for the multiplication to be associative is unnecessarily restrictive. There are important classes of star-algebra which are not associative (e.g. JB*-algebras). This PR removes the requirement for a `StarSemigroup` to be a semigroup, merely requiring it to have a multiplication. I've changed the name from `StarSemigroup` to `StarMul` since it's no longer a semigroup. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/non-associative.20*-algebras) Previously opened as a mathlib PR leanprover-community/mathlib#17949 Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com> 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. |
bors
bot
changed the title
Typically a * operation on a mathematical structure
Requipped with a multiplication is an involutive anti-automorphism i.e.Currently mathlib defines a class
StarSemigroupto be a semigroup satisfying this property. However, the requirement for the multiplication to be associative is unnecessarily restrictive. There are important classes of star-algebra which are not associative (e.g. JB*-algebras).This PR removes the requirement for a
StarSemigroupto be a semigroup, merely requiring it to have a multiplication.I've changed the name from
StarSemigrouptoStarMulsince it's no longer a semigroup.Zulip discussion
Previously opened as a mathlib PR leanprover-community/mathlib#17949