`prime_fivehundredsixtythree`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

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
2430
2431/-! ### 5-almost primes (Ω(n) = 5) -/
2432
2433/-- A number is 5-almost prime if Ω(n) = 5. -/
2434def isFiveAlmostPrime (n : ℕ) : Bool := bigOmega n = 5
2435
2436/-- 32 = 2⁵ is 5-almost prime. -/
2437theorem five_almost_prime_thirtytwo : isFiveAlmostPrime 32 = true := by native_decide
2438
2439/-- 48 = 2⁴ × 3 is 5-almost prime. -/
2440theorem five_almost_prime_fortyeight : isFiveAlmostPrime 48 = true := by native_decide
2441

papers checked against this theorem

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