Commit 2024-06-27 05:39 9c4c6f78

feat(SetTheory/Surreal/Basic): surreal number multiplication (#14044) 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 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.