Skip to content

Commit

Permalink
chore(algebra/ordered_group): move monoid stuff to ordered_monoid.lean (
Browse files Browse the repository at this point in the history 
#5066)

Replace one 2000 line file with two 1000 line files: ordered group stuff in one, and ordered monoid stuff in the other.
  • Loading branch information
@kbuzzard
kbuzzard committed Nov 22, 2020
1 parent 8d71ec9 commit 2a876b6
Show file tree
Hide file tree
Showing 2 changed files with 1,007 additions and 968 deletions.
Loading

0 comments on commit 2a876b6

Please sign in to comment.