mathlib
493cee78 - switch to general version of normality modulo one sorry

Commit

3 years ago

switch to general version of normality modulo one sorry

References

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

Author

alexjbest

alexjbest

Parents

Loading