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

Open

Commits

initial theorem of fuchs

alexjbest committed 4 years ago
sorry free

alexjbest committed 4 years ago
bit of clean up

alexjbest committed 4 years ago
make multiplicative

alexjbest committed 4 years ago
switch to general version of normality modulo one sorry

alexjbest committed 4 years ago
more homog version

alexjbest committed 4 years ago
generalizing to cancel monoids is now trivial

alexjbest committed 4 years ago
random workings

alexjbest committed 4 years ago
bits

alexjbest committed 4 years ago