theorem
proved
sigma_three_two
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 1832.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1829theorem sigma_three_one : sigma 3 1 = 1 := by native_decide
1830
1831/-- σ_3(2) = 1 + 8 = 9. -/
1832theorem sigma_three_two : sigma 3 2 = 9 := by native_decide
1833
1834/-- σ_3(3) = 1 + 27 = 28. -/
1835theorem sigma_three_three : sigma 3 3 = 28 := by native_decide
1836
1837/-- σ_3(4) = 1 + 8 + 64 = 73. -/
1838theorem sigma_three_four : sigma 3 4 = 73 := by native_decide
1839
1840/-- σ_3(5) = 1 + 125 = 126. -/
1841theorem sigma_three_five : sigma 3 5 = 126 := by native_decide
1842
1843/-- σ_3(6) = 1 + 8 + 27 + 216 = 252. -/
1844theorem sigma_three_six : sigma 3 6 = 252 := by native_decide
1845
1846/-- σ_3(8) = 1 + 8 + 64 + 512 = 585. -/
1847theorem sigma_three_eight : sigma 3 8 = 585 := by native_decide
1848
1849/-- σ_3(10) = 1 + 8 + 125 + 1000 = 1134. -/
1850theorem sigma_three_ten : sigma 3 10 = 1134 := by native_decide
1851
1852/-- σ_3(12) = 2044. -/
1853theorem sigma_three_twelve : sigma 3 12 = 2044 := by native_decide
1854
1855/-! ### Mod 6 prime classification (all primes > 3 are ≡ 1 or 5 mod 6) -/
1856
1857/-- 7 ≡ 1 (mod 6). -/
1858theorem mod6_seven_prime : Prime 7 ∧ 7 % 6 = 1 := by native_decide
1859
1860/-- 13 ≡ 1 (mod 6). -/
1861theorem mod6_thirteen_prime : Prime 13 ∧ 13 % 6 = 1 := by native_decide
1862