theorem
proved
prime_triplet_seven_eleven_thirteen
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 1541.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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². -/
1558theorem sum_of_squares_five : (5 : ℕ) = 1^2 + 2^2 := by native_decide
1559
1560/-- 13 = 2² + 3². -/
1561theorem sum_of_squares_thirteen : (13 : ℕ) = 2^2 + 3^2 := by native_decide
1562
1563/-- 17 = 1² + 4². -/
1564theorem sum_of_squares_seventeen : (17 : ℕ) = 1^2 + 4^2 := by native_decide
1565
1566/-- 29 = 2² + 5². -/
1567theorem sum_of_squares_twentynine : (29 : ℕ) = 2^2 + 5^2 := by native_decide
1568
1569/-- 37 = 1² + 6². -/
1570theorem sum_of_squares_thirtyseven : (37 : ℕ) = 1^2 + 6^2 := by native_decide
1571