Theorem Nat.abundant_iff_two_lt_abundancyIndex

Modification history

2026-01-29 03:31
Mathlib/NumberTheory/FactorisationProperties.lean
feat(NumberTheory/FactorizationProperties): Infinite abundant numbers, then golf (#34109)
Added Nat.abundant_iff_two_lt_abundancyIndexView on Github →