theorem
proved
mod4_three_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 1598.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1595/-! ### Primes p ≡ 3 (mod 4) — not expressible as sum of two squares -/
1596
1597/-- 3 ≡ 3 (mod 4). -/
1598theorem mod4_three_prime : Prime 3 ∧ 3 % 4 = 3 := by native_decide
1599
1600/-- 7 ≡ 3 (mod 4). -/
1601theorem mod4_seven_prime : Prime 7 ∧ 7 % 4 = 3 := by native_decide
1602
1603/-- 11 ≡ 3 (mod 4). -/
1604theorem mod4_eleven_prime : Prime 11 ∧ 11 % 4 = 3 := by native_decide
1605
1606/-- 19 ≡ 3 (mod 4). -/
1607theorem mod4_nineteen_prime : Prime 19 ∧ 19 % 4 = 3 := by native_decide
1608
1609/-- 23 ≡ 3 (mod 4). -/
1610theorem mod4_twentythree_prime : Prime 23 ∧ 23 % 4 = 3 := by native_decide
1611
1612/-- 31 ≡ 3 (mod 4). -/
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