Commit 2026-04-19 11:36 0f22cd14

View on Github →

refactor: golf only FactorisationProperties (#38204) This PR selectively ports part of #38144 and only migrates the changes in:

  • Mathlib/NumberTheory/FactorisationProperties.lean Concretely, this PR:
  • rewrites Prime.not_pseudoperfect to use Prime.properDivisors and Finset.sum_le_sum_of_subset directly, instead of analyzing the powerset of proper divisors by cases
  • shortens Prime.not_perfect to the direct consequence of Prime.not_pseudoperfect
  • refactors Prime.deficient_pow to reuse properDivisors_prime_pow and a simple mapped-sum identity, instead of reproving the structure of the proper divisors of a prime power inline

Estimated changes

modified theorem Nat.Prime.not_perfect