theorem
proved
mod4_fortythree_prime
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 1616.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1613theorem mod4_thirtyone_prime : Prime 31 ∧ 31 % 4 = 3 := by native_decide
1614
1615/-- 43 ≡ 3 (mod 4). -/
1616theorem mod4_fortythree_prime : Prime 43 ∧ 43 % 4 = 3 := by native_decide
1617
1618/-- 47 ≡ 3 (mod 4). -/
1619theorem mod4_fortyseven_prime : Prime 47 ∧ 47 % 4 = 3 := by native_decide
1620
1621/-- 59 ≡ 3 (mod 4). -/
1622theorem mod4_fiftynine_prime : Prime 59 ∧ 59 % 4 = 3 := by native_decide
1623
1624/-- 67 ≡ 3 (mod 4). -/
1625theorem mod4_sixtyseven_prime : Prime 67 ∧ 67 % 4 = 3 := by native_decide
1626
1627/-- 71 ≡ 3 (mod 4). -/
1628theorem mod4_seventyone_prime : Prime 71 ∧ 71 % 4 = 3 := by native_decide
1629
1630/-- 79 ≡ 3 (mod 4). -/
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