mathlib3
4bcba0da - chore(algebra/order/group/defs): split file (#17787)

Commit
3 years ago
chore(algebra/order/group/defs): split file (#17787) Splits: * algebra/order/group/defs.lean * algebra/group/with_one.lean * algebra/order/monoid/with_zero.lean This will get us unstuck on the mathlib4 port, moving some of the files (about algebraic morphisms and equivalences) that are currently waiting for fixes in Lean 4 off the critical path. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading