theorem
proved
vp_factorial_twentyfive_five
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 916.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
913theorem vp_factorial_twelve_three : vp 3 (Nat.factorial 12) = 5 := by native_decide
914
915/-- vp 5 (25!) = 6. -/
916theorem vp_factorial_twentyfive_five : vp 5 (Nat.factorial 25) = 6 := by native_decide
917
918/-- vp 7 (50!) = 8. -/
919theorem vp_factorial_fifty_seven : vp 7 (Nat.factorial 50) = 8 := by native_decide
920
921/-! ### More squarefree concrete values -/
922
923/-- 30 is squarefree. -/
924theorem squarefree_thirty : Squarefree 30 := by native_decide
925
926/-- 6 is squarefree. -/
927theorem squarefree_six : Squarefree 6 := by native_decide
928
929/-- 10 is squarefree. -/
930theorem squarefree_ten : Squarefree 10 := by native_decide
931
932/-- 15 is squarefree. -/
933theorem squarefree_fifteen : Squarefree 15 := by native_decide
934
935/-- 210 = 2×3×5×7 is squarefree. -/
936theorem squarefree_twohundredten : Squarefree 210 := by native_decide
937
938/-! ### Divisor count for RS constants -/
939
940/-- The number of divisors of 8 is 4. -/
941theorem divisors_card_eight : (8 : ℕ).divisors.card = 4 := by native_decide
942
943/-- The number of divisors of 45 is 6. -/
944theorem divisors_card_fortyfive : (45 : ℕ).divisors.card = 6 := by native_decide
945
946/-- The number of divisors of 360 is 24. -/