`prime_sixhundredseven`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 2630 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2630.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

2627theorem prime_sixhundredone : Prime 601 := by native_decide
2628
2629/-- 607 is prime. -/
2630theorem prime_sixhundredseven : Prime 607 := by native_decide
2631
2632/-- 613 is prime. -/
2633theorem prime_sixhundredthirteen : Prime 613 := by native_decide
2634
2635/-- 617 is prime. -/
2636theorem prime_sixhundredseventeen : Prime 617 := by native_decide
2637
2638/-- 619 is prime. -/
2639theorem prime_sixhundrednineteen : Prime 619 := by native_decide
2640
2641/-- 631 is prime. -/
2642theorem prime_sixhundredthirtyone : Prime 631 := by native_decide
2643
2644/-- 641 is prime (Fermat prime related: divides F₅). -/
2645theorem prime_sixhundredfortyone : Prime 641 := by native_decide
2646
2647/-- 643 is prime. -/
2648theorem prime_sixhundredfortythree : Prime 643 := by native_decide
2649
2650/-- 647 is prime. -/
2651theorem prime_sixhundredfortyseven : Prime 647 := by native_decide
2652
2653/-- 653 is prime. -/
2654theorem prime_sixhundredfiftythree : Prime 653 := by native_decide
2655
2656/-- 659 is prime. -/
2657theorem prime_sixhundredfiftynine : Prime 659 := by native_decide
2658
2659/-- 661 is prime. -/
2660theorem prime_sixhundredsixtyone : Prime 661 := by native_decide

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.