theorem
proved
deficient_seven
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 1471.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
1487/-- 5 ≡ 1 (mod 4) is a Pythagorean prime. -/
1488theorem pythagorean_prime_five : Prime 5 ∧ 5 % 4 = 1 := by native_decide
1489
1490/-- 13 ≡ 1 (mod 4) is a Pythagorean prime. -/
1491theorem pythagorean_prime_thirteen : Prime 13 ∧ 13 % 4 = 1 := by native_decide
1492
1493/-- 17 ≡ 1 (mod 4) is a Pythagorean prime. -/
1494theorem pythagorean_prime_seventeen : Prime 17 ∧ 17 % 4 = 1 := by native_decide
1495
1496/-- 29 ≡ 1 (mod 4) is a Pythagorean prime. -/
1497theorem pythagorean_prime_twentynine : Prime 29 ∧ 29 % 4 = 1 := by native_decide
1498
1499/-- 37 ≡ 1 (mod 4) is a Pythagorean prime. -/
1500theorem pythagorean_prime_thirtyseven : Prime 37 ∧ 37 % 4 = 1 := by native_decide
1501