[Merged by Bors] - feat(SetTheory/Surreal/Basic): surreal number multiplication#14044
[Merged by Bors] - feat(SetTheory/Surreal/Basic): surreal number multiplication#14044
Conversation
PR summary 877c8d3e90Import changesDependency changes
|
766cd86 to
36c6cd7
Compare
alreadydone
left a comment
There was a problem hiding this comment.
Thanks for porting and opening the PR! Here are some initial comments, and I'll probably do some cleanups myself later. (There's a algebraic geometry formalization workshop this week, so my time will be limited ...)
…leanprover-community/mathlib4 into hwatheod/surreal_multiplication
alreadydone
left a comment
There was a problem hiding this comment.
Thanks for your work! I've pushed some more cleanups. I think the only thing remaining is to clean up the draft docs, which I should be able to do by the end of tomorrow.
There was a problem hiding this comment.
Okay I think I've done cleaning up the PR. Maybe @MichaelStollBayreuth (coauthor of the original proof) would be interested in taking a look, and then I think we can merge this!
|
Also, I haven't seen @vihdzp around for a while but I think this is worth a notification. also cc @apurvanakade |
|
I'll try to have a look soon-ish, but won't have a lot of time this week because of the AIM workshop (plus teaching etc. as usual). |
|
Two minor comments, but otherwise I'm happy. bors d+ |
|
✌️ hwatheod can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
prove multiplication of surreal numbers is well-defined, thus they form an ordered commutative ring This is a port of a Lean 3 proof from [this mathlib branch](https://github.com/leanprover-community/mathlib/blob/surreal_mul_symm'/src/set_theory/surreal/basic.lean). It shows that multiplication of surreal numbers is well-defined, and therefore the surreal numbers form an ordered commutative ring. Because `Surreal` is now a ring, the simp normal-form for scalar multiplication (by integers) is now `*`. This required changes throughout `SetTheory/Surreal/Dyadic`. For the most part, I translated the Lean 3 code directly to Lean 4, although in a few cases, I couldn't get that to work and wrote a new proof instead. There were some lemmas used that were in the mathlib branch that were not ported to mathlib4. I have ported those lemmas and put them in an appropriate place in mathlib4. I copied over the author names from the Lean 3 code and added myself. Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
prove multiplication of surreal numbers is well-defined, thus they form an ordered commutative ring This is a port of a Lean 3 proof from [this mathlib branch](https://github.com/leanprover-community/mathlib/blob/surreal_mul_symm'/src/set_theory/surreal/basic.lean). It shows that multiplication of surreal numbers is well-defined, and therefore the surreal numbers form an ordered commutative ring. Because `Surreal` is now a ring, the simp normal-form for scalar multiplication (by integers) is now `*`. This required changes throughout `SetTheory/Surreal/Dyadic`. For the most part, I translated the Lean 3 code directly to Lean 4, although in a few cases, I couldn't get that to work and wrote a new proof instead. There were some lemmas used that were in the mathlib branch that were not ported to mathlib4. I have ported those lemmas and put them in an appropriate place in mathlib4. I copied over the author names from the Lean 3 code and added myself. Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Deduplicates the instance `LinearOrder Surreal`, which was defined in both `Surreal/Basic` and `Surreal/Multiplication`. The duplicate originated in #14044. The surviving instance is at https://github.com/leanprover-community/mathlib4/blob/461b2e79dd4c923f26e435f770faeaf87208d0d9/Mathlib/SetTheory/Surreal/Basic.lean#L368-L373
Deduplicates the instance `LinearOrder Surreal`, which was defined in both `Surreal/Basic` and `Surreal/Multiplication`. The duplicate originated in #14044. The surviving instance is at https://github.com/leanprover-community/mathlib4/blob/461b2e79dd4c923f26e435f770faeaf87208d0d9/Mathlib/SetTheory/Surreal/Basic.lean#L368-L373
prove multiplication of surreal numbers is well-defined, thus they form an ordered commutative ring
This is a port of a Lean 3 proof from this mathlib branch. It shows that multiplication of surreal numbers is well-defined, and therefore the surreal numbers form an ordered commutative ring.
Because
Surrealis now a ring, the simp normal-form for scalar multiplication (by integers) is now*. This required changes throughoutSetTheory/Surreal/Dyadic.For the most part, I translated the Lean 3 code directly to Lean 4, although in a few cases, I couldn't get that to work and wrote a new proof instead.
There were some lemmas used that were in the mathlib branch that were not ported to mathlib4. I have ported those lemmas and put them in an appropriate place in mathlib4.
I copied over the author names from the Lean 3 code and added myself.