`prime_fourhundredsixtyseven`

proved

show as: view math explainer →

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

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

2199theorem prime_fourhundredsixtythree : Prime 463 := by native_decide
2200
2201/-- 467 is prime. -/
2202theorem prime_fourhundredsixtyseven : Prime 467 := by native_decide
2203
2204/-- 479 is prime. -/
2205theorem prime_fourhundredseventynine : Prime 479 := by native_decide
2206
2207/-- 487 is prime. -/
2208theorem prime_fourhundredeightyseven : Prime 487 := by native_decide
2209
2210/-- 491 is prime. -/
2211theorem prime_fourhundredninetyone : Prime 491 := by native_decide
2212
2213/-- 499 is prime. -/
2214theorem prime_fourhundredninetynine : Prime 499 := by native_decide
2215
2216/-! ### 4-almost primes (Ω(n) = 4) -/
2217
2218/-- A number is 4-almost prime if Ω(n) = 4. -/
2219def isFourAlmostPrime (n : ℕ) : Bool := bigOmega n = 4
2220
2221/-- 16 = 2⁴ is 4-almost prime. -/
2222theorem four_almost_prime_sixteen : isFourAlmostPrime 16 = true := by native_decide
2223
2224/-- 24 = 2³ × 3 is 4-almost prime. -/
2225theorem four_almost_prime_twentyfour : isFourAlmostPrime 24 = true := by native_decide
2226
2227/-- 36 = 2² × 3² is 4-almost prime. -/
2228theorem four_almost_prime_thirtysix : isFourAlmostPrime 36 = true := by native_decide
2229
2230/-- 40 = 2³ × 5 is 4-almost prime. -/
2231theorem four_almost_prime_forty : isFourAlmostPrime 40 = true := by native_decide
2232

papers checked against this theorem

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