theorem
proved
abundant_twenty
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 1442.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1439theorem abundant_eighteen : sigma 1 18 > 2 * 18 := by native_decide
1440
1441/-- 20 is abundant: σ_1(20) = 42 > 40. -/
1442theorem abundant_twenty : sigma 1 20 > 2 * 20 := by native_decide
1443
1444/-- 24 is abundant: σ_1(24) = 60 > 48. -/
1445theorem abundant_twentyfour : sigma 1 24 > 2 * 24 := by native_decide
1446
1447/-- 30 is abundant: σ_1(30) = 72 > 60. -/
1448theorem abundant_thirty : sigma 1 30 > 2 * 30 := by native_decide
1449
1450/-- 36 is abundant: σ_1(36) = 91 > 72. -/
1451theorem abundant_thirtysix : sigma 1 36 > 2 * 36 := by native_decide
1452
1453/-! ### Deficient numbers (σ_1(n) < 2n) -/
1454
1455/-- 1 is deficient: σ_1(1) = 1 < 2. -/
1456theorem deficient_one : sigma 1 1 < 2 * 1 := by native_decide
1457
1458/-- 2 is deficient: σ_1(2) = 3 < 4. -/
1459theorem deficient_two : sigma 1 2 < 2 * 2 := by native_decide
1460
1461/-- 3 is deficient: σ_1(3) = 4 < 6. -/
1462theorem deficient_three : sigma 1 3 < 2 * 3 := by native_decide
1463
1464/-- 4 is deficient: σ_1(4) = 7 < 8. -/
1465theorem deficient_four : sigma 1 4 < 2 * 4 := by native_decide
1466
1467/-- 5 is deficient: σ_1(5) = 6 < 10. -/
1468theorem deficient_five : sigma 1 5 < 2 * 5 := by native_decide
1469
1470/-- 7 is deficient: σ_1(7) = 8 < 14. -/
1471theorem deficient_seven : sigma 1 7 < 2 * 7 := by native_decide
1472