theorem
proved
pythagorean_prime_onehundredthirteen
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 1527.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1524theorem pythagorean_prime_onehundrednine : Prime 109 ∧ 109 % 4 = 1 := by native_decide
1525
1526/-- 113 ≡ 1 (mod 4) is a Pythagorean prime. -/
1527theorem pythagorean_prime_onehundredthirteen : Prime 113 ∧ 113 % 4 = 1 := by native_decide
1528
1529/-- 137 ≡ 1 (mod 4) is a Pythagorean prime (RS-relevant). -/
1530theorem pythagorean_prime_onehundredthirtyseven : Prime 137 ∧ 137 % 4 = 1 := by native_decide
1531
1532/-! ### Prime triplets (three primes with gaps ≤ 6) -/
1533
1534/-- (3, 5, 7) is a prime triplet. -/
1535theorem prime_triplet_three_five_seven : Prime 3 ∧ Prime 5 ∧ Prime 7 := by native_decide
1536
1537/-- (5, 7, 11) are three primes with gap (2, 4). -/
1538theorem prime_triplet_five_seven_eleven : Prime 5 ∧ Prime 7 ∧ Prime 11 := by native_decide
1539
1540/-- (7, 11, 13) are three primes with gap (4, 2). -/
1541theorem prime_triplet_seven_eleven_thirteen : Prime 7 ∧ Prime 11 ∧ Prime 13 := by native_decide
1542
1543/-- (11, 13, 17) are three primes with gap (2, 4). -/
1544theorem prime_triplet_eleven_thirteen_seventeen : Prime 11 ∧ Prime 13 ∧ Prime 17 := by native_decide
1545
1546/-- (13, 17, 19) are three primes with gap (4, 2). -/
1547theorem prime_triplet_thirteen_seventeen_nineteen : Prime 13 ∧ Prime 17 ∧ Prime 19 := by native_decide
1548
1549/-- (17, 19, 23) are three primes with gap (2, 4). -/
1550theorem prime_triplet_seventeen_nineteen_twentythree : Prime 17 ∧ Prime 19 ∧ Prime 23 := by native_decide
1551
1552/-- (37, 41, 43) are three primes with gap (4, 2). RS-relevant (37 is the beat numerator). -/
1553theorem prime_triplet_thirtyseven_fortyone_fortythree : Prime 37 ∧ Prime 41 ∧ Prime 43 := by native_decide
1554
1555/-! ### Sum of two squares representations for Pythagorean primes -/
1556
1557/-- 5 = 1² + 2². -/