theorem
proved
palindromic_prime_onehundredone
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 2498.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
2509/-- 191 is a palindromic prime. -/
2510theorem palindromic_prime_onehundredninetyone : Prime 191 := by native_decide
2511
2512/-- 313 is a palindromic prime. -/
2513theorem palindromic_prime_threehundredthirteen : Prime 313 := by native_decide
2514
2515/-- 353 is a palindromic prime. -/
2516theorem palindromic_prime_threehundredfiftythree : Prime 353 := by native_decide
2517
2518/-- 373 is a palindromic prime. -/
2519theorem palindromic_prime_threehundredseventythree : Prime 373 := by native_decide
2520
2521/-- 383 is a palindromic prime. -/
2522theorem palindromic_prime_threehundredeightythree : Prime 383 := by native_decide
2523
2524/-- 727 is a palindromic prime. -/
2525theorem palindromic_prime_sevenhundredtwentyseven : Prime 727 := by native_decide
2526
2527/-- 757 is a palindromic prime. -/
2528theorem palindromic_prime_sevenhundredfiftyseven : Prime 757 := by native_decide