theorem
proved
deficient_one
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 1456.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
1473/-- 8 is deficient: σ_1(8) = 15 < 16. -/
1474theorem deficient_eight : sigma 1 8 < 2 * 8 := by native_decide
1475
1476/-- 9 is deficient: σ_1(9) = 13 < 18. -/
1477theorem deficient_nine : sigma 1 9 < 2 * 9 := by native_decide
1478
1479/-- 10 is deficient: σ_1(10) = 18 < 20. -/
1480theorem deficient_ten : sigma 1 10 < 2 * 10 := by native_decide
1481
1482/-- 11 is deficient (all primes are deficient). -/
1483theorem deficient_eleven : sigma 1 11 < 2 * 11 := by native_decide
1484
1485/-! ### Pythagorean primes (p ≡ 1 mod 4) — can be expressed as sum of two squares -/
1486