theorem
proved
five_almost_prime_twohundredseventytwo
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 2478.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2475theorem five_almost_prime_twohundredfortythree : isFiveAlmostPrime 243 = true := by native_decide
2476
2477/-- 272 = 2⁴ × 17 is 5-almost prime (RS-relevant: 17). -/
2478theorem five_almost_prime_twohundredseventytwo : isFiveAlmostPrime 272 = true := by native_decide
2479
2480/-! ### Palindromic primes -/
2481
2482/-- 2 is a palindromic prime (single digit). -/
2483theorem palindromic_prime_two : Prime 2 := by native_decide
2484
2485/-- 3 is a palindromic prime (single digit). -/
2486theorem palindromic_prime_three : Prime 3 := by native_decide
2487
2488/-- 5 is a palindromic prime (single digit). -/
2489theorem palindromic_prime_five : Prime 5 := by native_decide
2490
2491/-- 7 is a palindromic prime (single digit). -/
2492theorem palindromic_prime_seven : Prime 7 := by native_decide
2493
2494/-- 11 is a palindromic prime (RS-relevant). -/
2495theorem palindromic_prime_eleven : Prime 11 := by native_decide
2496
2497/-- 101 is a palindromic prime. -/
2498theorem palindromic_prime_onehundredone : Prime 101 := by native_decide
2499
2500/-- 131 is a palindromic prime. -/
2501theorem palindromic_prime_onehundredthirtyone : Prime 131 := by native_decide
2502
2503/-- 151 is a palindromic prime. -/
2504theorem palindromic_prime_onehundredfiftyone : Prime 151 := by native_decide
2505
2506/-- 181 is a palindromic prime. -/
2507theorem palindromic_prime_onehundredeightyone : Prime 181 := by native_decide
2508