`prime_fivehundredtwentythree`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 2399 · 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 2399.

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

2396theorem prime_fivehundredtwentyone : Prime 521 := by native_decide
2397
2398/-- 523 is prime. -/
2399theorem prime_fivehundredtwentythree : Prime 523 := by native_decide
2400
2401/-- 541 is prime. -/
2402theorem prime_fivehundredfortyone : Prime 541 := by native_decide
2403
2404/-- 547 is prime. -/
2405theorem prime_fivehundredfortyseven : Prime 547 := by native_decide
2406
2407/-- 557 is prime. -/
2408theorem prime_fivehundredfiftyseven : Prime 557 := by native_decide
2409
2410/-- 563 is prime (Wilson prime). -/
2411theorem prime_fivehundredsixtythree : Prime 563 := by native_decide
2412
2413/-- 569 is prime. -/
2414theorem prime_fivehundredsixtynine : Prime 569 := by native_decide
2415
2416/-- 571 is prime. -/
2417theorem prime_fivehundredseventyone : Prime 571 := by native_decide
2418
2419/-- 577 is prime. -/
2420theorem prime_fivehundredseventyseven : Prime 577 := by native_decide
2421
2422/-- 587 is prime. -/
2423theorem prime_fivehundredeightyseven : Prime 587 := by native_decide
2424
2425/-- 593 is prime. -/
2426theorem prime_fivehundredninetythree : Prime 593 := by native_decide
2427
2428/-- 599 is prime. -/
2429theorem prime_fivehundredninetynine : Prime 599 := by native_decide

papers checked against this theorem

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