Commit 2026-06-26 12:41 d6772ece

feat(Data/Nat): a number divides a power of its own radical (#40170) A few factorization lemmas, including:

• ∀ n : ℕ, n ∣ radical n ^ n
• ∀ n k : ℕ, n ∣ k ^ n ↔ n.primeFactors ⊆ k.primeFactors
• ∀ n k : ℕ, radical n ∣ k ↔ n.primeFactors ⊆ k.primeFactors
• In any UniqueFactorizationMonoid M, ∀ a : M, ∃ n, a ∣ radical a ^ n #Is there code for X? > A number divides a power of its square-free component