theorem
proved
sigma_two_ten
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 1663.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
1673/-- π(400) = 78. -/
1674theorem primeCounting_fourhundred : primeCounting 400 = 78 := by native_decide
1675
1676/-- π(600) = 109. -/
1677theorem primeCounting_sixhundred : primeCounting 600 = 109 := by native_decide
1678
1679/-- π(800) = 139. -/
1680theorem primeCounting_eighthundred : primeCounting 800 = 139 := by native_decide
1681
1682/-- π(900) = 154. -/
1683theorem primeCounting_ninehundred : primeCounting 900 = 154 := by native_decide
1684
1685/-! ### More sum of squares representations -/
1686
1687/-- 61 = 5² + 6². -/
1688theorem sum_of_squares_sixtyone : (61 : ℕ) = 5^2 + 6^2 := by native_decide
1689
1690/-- 73 = 3² + 8². -/
1691theorem sum_of_squares_seventythree : (73 : ℕ) = 3^2 + 8^2 := by native_decide
1692
1693/-- 89 = 5² + 8². -/