theorem
proved
mod4_eightythree_prime
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 1634.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1631theorem mod4_seventynine_prime : Prime 79 ∧ 79 % 4 = 3 := by native_decide
1632
1633/-- 83 ≡ 3 (mod 4). -/
1634theorem mod4_eightythree_prime : Prime 83 ∧ 83 % 4 = 3 := by native_decide
1635
1636/-- 103 ≡ 3 (mod 4) (RS-relevant). -/
1637theorem mod4_onehundredthree_prime : Prime 103 ∧ 103 % 4 = 3 := by native_decide
1638
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