theorem
proved
mobius_onehundredfive
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 1119.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1116theorem mobius_seventy : mobius 70 = -1 := by native_decide
1117
1118/-- μ(105) = -1 (squarefree with 3 prime factors). -/
1119theorem mobius_onehundredfive : mobius 105 = -1 := by native_decide
1120
1121/-- μ(210) = 1 (squarefree with 4 prime factors). -/
1122theorem mobius_twohundredten : mobius 210 = 1 := by native_decide
1123
1124/-- μ(18) = 0 (not squarefree, 9 | 18). -/
1125theorem mobius_eighteen : mobius 18 = 0 := by native_decide
1126
1127/-- μ(20) = 0 (not squarefree, 4 | 20). -/
1128theorem mobius_twenty : mobius 20 = 0 := by native_decide
1129
1130/-! ### More squarefree values -/
1131
1132/-- 42 = 2×3×7 is squarefree. -/
1133theorem squarefree_fortytwo : Squarefree 42 := by native_decide
1134
1135/-- 70 = 2×5×7 is squarefree. -/
1136theorem squarefree_seventy : Squarefree 70 := by native_decide
1137
1138/-- 105 = 3×5×7 is squarefree. -/
1139theorem squarefree_onehundredfive : Squarefree 105 := by native_decide
1140
1141/-- 77 = 7×11 is squarefree. -/
1142theorem squarefree_seventyseven : Squarefree 77 := by native_decide
1143
1144/-- 91 = 7×13 is squarefree. -/
1145theorem squarefree_ninetyone : Squarefree 91 := by native_decide
1146
1147/-- 35 = 5×7 is squarefree. -/
1148theorem squarefree_thirtyfive : Squarefree 35 := by native_decide
1149