Commit 2025-10-01 20:18 69ebb748

perf(Algebra/IsPrimePow): speed up decidability for Nat IsPrimePow (#30093) Previously, this decidability instance was defined using isPrimePow_nat_iff_bounded, which (as I understand it) means that it undertook a search over all pairs p, k of numbers below n until it finds one where p is prime, and p^k = n, or else loops through all possibilities. This PR creates a new theorem which instead searches over possible values of the exponent first, bounding the search at the binary logarithm of n, and then a further theorem which uses n.minFac for p. This massively reduces the time for large n. In principle this could be made polynomial time, if we were to compute the putative prime factor for each k by taking the kth root and checking primality with AKS. But until that is implemented, this seems like a fine improvement.