mathlib3
eb2dcba5 - refactor(*): remove uses of omega in the library (#6129)

Commit

4 years ago

refactor(*): remove uses of omega in the library (#6129) The transition to Lean 4 will be easier if we don't have to port omega.

Author

sgouezel

Parents