`prime_fourhundredfortynine`

proved

show as: view math explainer →

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

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

2187theorem prime_fourhundredfortythree : Prime 443 := by native_decide
2188
2189/-- 449 is prime. -/
2190theorem prime_fourhundredfortynine : Prime 449 := by native_decide
2191
2192/-- 457 is prime. -/
2193theorem prime_fourhundredfiftyseven : Prime 457 := by native_decide
2194
2195/-- 461 is prime. -/
2196theorem prime_fourhundredsixtyone : Prime 461 := by native_decide
2197
2198/-- 463 is prime. -/
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

papers checked against this theorem

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