theorem
proved
sigma_two_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 1642.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1639/-! ### σ_2 values (sum of squares of divisors) -/
1640
1641/-- σ_2(1) = 1. -/
1642theorem sigma_two_one : sigma 2 1 = 1 := by native_decide
1643
1644/-- σ_2(2) = 1 + 4 = 5. -/
1645theorem sigma_two_two : sigma 2 2 = 5 := by native_decide
1646
1647/-- σ_2(3) = 1 + 9 = 10. -/
1648theorem sigma_two_three : sigma 2 3 = 10 := by native_decide
1649
1650/-- σ_2(4) = 1 + 4 + 16 = 21. -/
1651theorem sigma_two_four : sigma 2 4 = 21 := by native_decide
1652
1653/-- σ_2(5) = 1 + 25 = 26. -/
1654theorem sigma_two_five : sigma 2 5 = 26 := by native_decide
1655
1656/-- σ_2(6) = 1 + 4 + 9 + 36 = 50. -/
1657theorem sigma_two_six : sigma 2 6 = 50 := by native_decide
1658
1659/-- σ_2(8) = 1 + 4 + 16 + 64 = 85. -/
1660theorem sigma_two_eight : sigma 2 8 = 85 := by native_decide
1661
1662/-- σ_2(10) = 1 + 4 + 25 + 100 = 130. -/
1663theorem sigma_two_ten : sigma 2 10 = 130 := by native_decide
1664
1665/-- σ_2(12) = 1 + 4 + 9 + 16 + 36 + 144 = 210. -/
1666theorem sigma_two_twelve : sigma 2 12 = 210 := by native_decide
1667
1668/-- σ_2(30) = 1300 (divisors: 1+4+9+25+36+100+225+900). -/
1669theorem sigma_two_thirty : sigma 2 30 = 1300 := by native_decide
1670
1671/-! ### More primeCounting values at round numbers -/
1672