basic): split into two files, one not depending on the order hierarchy (#17174)

Commit

3 years ago

chore(data/nat/basic): split into two files, one not depending on the order hierarchy (#17174) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents

11dcb6b5

mathlib a3240c4f - chore(data/nat/basic): split into two files, one not depending on the order hierarchy (#17174)

mathlib
a3240c4f - chore(data/nat/basic): split into two files, one not depending on the order hierarchy (#17174)