Commit 2024-09-29 00:04 ba011604

View on Github →

feat(NumberTheory/FactorisationProperties): abundant, pseudoperfect, deficient, and weird numbers (#14269)

Estimated changes

added theorem IsPrimePow.deficient
added def Nat.Abundant
added def Nat.Deficient
added theorem Nat.Prime.deficient
added theorem Nat.Prime.not_abundant
added theorem Nat.Prime.not_perfect
added theorem Nat.Prime.not_weird
added def Nat.Weird
added theorem Nat.abundant_twelve
added theorem Nat.deficient_one
added theorem Nat.deficient_three
added theorem Nat.deficient_two
added theorem Nat.infinite_deficient
added theorem Nat.weird_seventy