Commit 2022-02-24 00:24 620af85a

refactor(topology/instances): put ℕ, ℤ, and ℚ in separate files (#12207) The goal here is to make metric_space ℕ and metric_space ℤ available earlier, so that I can state has_bounded_smul ℕ A somewhere reasonable. No lemmas have been added, deleted, or changed here - they've just been moved out of topology/instances/real and into topology/instances/{nat,int,rat,real}. The resulting import structure is:

• rat_lemmas → rat
• rat → {real, int, nat}
• real → {int}
• nat → {int}