mathlib3
7fdd4f37 - refactor(data/nat/nth): redefine, review API (#18760)

Commit
2 years ago
refactor(data/nat/nth): redefine, review API (#18760) Redefine `nat.nth` in terms of already available definitions, review API, generalize some lemmas. Also fix some typos in `data/set/intervals/monotone`.
Author
Parents
Loading