Commit 2026-01-29 03:31 b6f92650

View on Github →

feat(NumberTheory/FactorizationProperties): Infinite abundant numbers, then golf (#34109)

Estimated changes

Modified Mathlib/NumberTheory/FactorisationProperties.lean

added theorem Nat.Abundant.mul_left

added theorem Nat.Abundant.of_dvd

modified theorem Nat.Prime.deficient

added def Nat.abundancyIndex

added theorem Nat.abundancyIndex_le_of_dvd

added theorem Nat.abundant_iff_sum_divisors

added theorem Nat.abundant_iff_two_lt_abundancyIndex

modified theorem Nat.deficient_one

modified theorem Nat.deficient_three

modified theorem Nat.deficient_two

added theorem Nat.infinite_even_abundant

added theorem Nat.infinite_odd_abundant

added theorem Nat.not_abundant_zero