theorem
proved
mobius_twenty
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 1128.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
1150/-- 21 = 3×7 is squarefree. -/
1151theorem squarefree_twentyone : Squarefree 21 := by native_decide
1152
1153/-- 33 = 3×11 is squarefree. -/
1154theorem squarefree_thirtythree : Squarefree 33 := by native_decide
1155
1156/-- 18 is NOT squarefree (9 | 18). -/
1157theorem not_squarefree_eighteen : ¬Squarefree 18 := by native_decide
1158