Commit 2024-07-03 08:52 fcfd70eb

chore(Data/Nat): refactor import of Nat/Prime by Nat/Factors (#14357) Further reduce imports of full Prime.lean. Here, Data.Nat.Factors now imports only Prime/Defs. For this, four lemmas had to be added to Prime/Defs from Prime/Basic. Many modules import Data.Nat.Factors, so their dependencies on Prime theorems are now uncovered. Still, this change will reduce the amount of what is imported, in general. Motivation is a circular dependency that would prevent me from adding a lemma to Prime/Basic.