theorem
proved
prime_sixtyone
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 560.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
557theorem prime_fortyseven : Prime 47 := by decide
558theorem prime_fiftythree : Prime 53 := by decide
559theorem prime_fiftynine : Prime 59 := by decide
560theorem prime_sixtyone : Prime 61 := by decide
561theorem prime_sixtyseven : Prime 67 := by decide
562theorem prime_seventyone : Prime 71 := by decide
563theorem prime_seventythree : Prime 73 := by decide
564theorem prime_seventynine : Prime 79 := by decide
565theorem prime_eightythree : Prime 83 := by decide
566theorem prime_eightynine : Prime 89 := by decide
567theorem prime_ninetyseven : Prime 97 := by decide
568
569/-! ### Factorial valuations (decidable facts) -/
570
571/-- vp 2 (4!) = 3. -/
572theorem vp_factorial_four_two : vp 2 (Nat.factorial 4) = 3 := by native_decide
573
574/-- vp 2 (5!) = 3. -/
575theorem vp_factorial_five_two : vp 2 (Nat.factorial 5) = 3 := by native_decide
576
577/-- vp 2 (6!) = 4. -/
578theorem vp_factorial_six_two : vp 2 (Nat.factorial 6) = 4 := by native_decide
579
580/-- vp 2 (8!) = 7. -/
581theorem vp_factorial_eight_two : vp 2 (Nat.factorial 8) = 7 := by native_decide
582
583/-- vp 3 (6!) = 2. -/
584theorem vp_factorial_six_three : vp 3 (Nat.factorial 6) = 2 := by native_decide
585
586/-- vp 3 (9!) = 4. -/
587theorem vp_factorial_nine_three : vp 3 (Nat.factorial 9) = 4 := by native_decide
588
589/-- vp 5 (10!) = 2. -/
590theorem vp_factorial_ten_five : vp 5 (Nat.factorial 10) = 2 := by native_decide