theorem
proved
prime_twohundredtwentynine
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 1944.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1941theorem prime_twohundredtwentyseven : Prime 227 := by native_decide
1942
1943/-- 229 is prime. -/
1944theorem prime_twohundredtwentynine : Prime 229 := by native_decide
1945
1946/-- 233 is prime. -/
1947theorem prime_twohundredthirtythree : Prime 233 := by native_decide
1948
1949/-- 239 is prime. -/
1950theorem prime_twohundredthirtynine : Prime 239 := by native_decide
1951
1952/-- 241 is prime. -/
1953theorem prime_twohundredfortyone : Prime 241 := by native_decide
1954
1955/-- 251 is prime. -/
1956theorem prime_twohundredfiftyone : Prime 251 := by native_decide
1957
1958/-- 257 is prime (Fermat prime F_3 = 2^8 + 1). -/
1959theorem prime_twohundredfiftyseven : Prime 257 := by native_decide
1960
1961/-- 263 is prime. -/
1962theorem prime_twohundredsixtythree : Prime 263 := by native_decide
1963
1964/-- 269 is prime. -/
1965theorem prime_twohundredsixtynine : Prime 269 := by native_decide
1966
1967/-- 271 is prime. -/
1968theorem prime_twohundredseventyone : Prime 271 := by native_decide
1969
1970/-- 277 is prime. -/
1971theorem prime_twohundredseventyseven : Prime 277 := by native_decide
1972
1973/-- 281 is prime. -/
1974theorem prime_twohundredeightyone : Prime 281 := by native_decide