mathlib
0ff989e5 - chore(algebra/group/basic): split file (#16847)

Commit
3 years ago
chore(algebra/group/basic): split file (#16847) Motivated by porting material on ordered_ring for linarith. Just stripping out tangential imports from files at the very bottom of the import thicket. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading