arienmalec
arienmalec
Updated Complex Number Game to use latest Lean 3 and `mathlib`. The "all in one" proof for `comm_ring` broke (presumably because the structure is more complicated in updated `mathlib`, so...
`mathlib` `RBTree` and `RBMap` won't be ported to `mathlib4` but some of the theorems there should eventually be covered in `Std`. In particular: https://github.com/leanprover-community/mathlib/blob/master/src/data/rbtree/basic.lean https://github.com/leanprover-community/mathlib/blob/master/src/data/rbtree/find.lean https://github.com/leanprover-community/mathlib/blob/master/src/data/rbtree/min_max.lean https://github.com/leanprover-community/mathlib/blob/master/src/data/rbmap/default.lean