mathlib3
feat(order/extension): extending ordered groups to linear ordered groups
#11897

Open

feat(order/extension): extending ordered groups to linear ordered groups #11897

alexjbest wants to merge 9 commits into master from alexjbest/fuchs

initial theorem of fuchs

dca51753

sorry free

159f6102

alexjbest added WIP

bit of clean up

b3df3739

make multiplicative

3bca6135

switch to general version of normality modulo one sorry

493cee78

more homog version

d70d52a1

generalizing to cancel monoids is now trivial

51f3676c

random workings

b812f1ce

bits

5cab2fac

kim-em added too-late

Reviewers

No reviews

Assignees

No one assigned

Labels

WIP too-late

Milestone

No milestone