Commit 2022-10-08 15:49 0ff989e5
View on Github →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.
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.