Commit 2024-10-25 20:03 eba9c377

chore(Data/Nat/Prime): split Defs; rearrange Basic (#18233) This PR reduces the theory included with Data/Nat/Prime/Defs.lean, in particular allowing us to define CharP without needing theory on ordered monoids. Most of the contents got moved to Basic.lean, which would increase the downstream imports for quite a few file. So in turn I split up Basic.lean based on the imports and logical structure:

• Results related to the factorial go to Prime/Factorial.lean
• Results related to integers go to Prime/Int.lean (which should probably be merged with `Data/Int/NatPrime.lean)
• The proof that there are infinitely many primes goes to Prime/Infinite.lean
• Some results on powers of prime that needed a higher amount of ordered monoid theory go to Prime/Pow.lean This is not a universal import win, since some files that imported Defs.lean now need to import Basic.lean instead, but I think that's worth it for keeping Defs files succinct.