Theorem Surreal.Multiplication.ih1_swap

Modification history

2024-07-28 23:33

Mathlib/SetTheory/Surreal/Multiplication.lean

chore: robustifying for debug.byAsSorry (part 13) (#15197)

Modified Surreal.Multiplication.ih1_swap View on Github →

2024-06-27 05:39

Mathlib/SetTheory/Surreal/Multiplication.lean

feat(SetTheory/Surreal/Basic): surreal number multiplication (#14044) …

Added Surreal.Multiplication.ih1_swap View on Github →