theorem
proved
sigma_three_eight
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 1847.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
1863/-- 19 ≡ 1 (mod 6). -/
1864theorem mod6_nineteen_prime : Prime 19 ∧ 19 % 6 = 1 := by native_decide
1865
1866/-- 31 ≡ 1 (mod 6). -/
1867theorem mod6_thirtyone_prime : Prime 31 ∧ 31 % 6 = 1 := by native_decide
1868
1869/-- 37 ≡ 1 (mod 6) (RS-relevant). -/
1870theorem mod6_thirtyseven_prime : Prime 37 ∧ 37 % 6 = 1 := by native_decide
1871
1872/-- 43 ≡ 1 (mod 6). -/
1873theorem mod6_fortythree_prime : Prime 43 ∧ 43 % 6 = 1 := by native_decide
1874
1875/-- 61 ≡ 1 (mod 6). -/
1876theorem mod6_sixtyone_prime : Prime 61 ∧ 61 % 6 = 1 := by native_decide
1877