theorem
proved
mobius_ten
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 1101.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1098/-! ### More Möbius values -/
1099
1100/-- μ(10) = 1 (squarefree with 2 prime factors). -/
1101theorem mobius_ten : mobius 10 = 1 := by native_decide
1102
1103/-- μ(15) = 1 (squarefree with 2 prime factors). -/
1104theorem mobius_fifteen : mobius 15 = 1 := by native_decide
1105
1106/-- μ(21) = 1 (squarefree with 2 prime factors). -/
1107theorem mobius_twentyone : mobius 21 = 1 := by native_decide
1108
1109/-- μ(35) = 1 (squarefree with 2 prime factors). -/
1110theorem mobius_thirtyfive : mobius 35 = 1 := by native_decide
1111
1112/-- μ(42) = -1 (squarefree with 3 prime factors). -/
1113theorem mobius_fortytwo : mobius 42 = -1 := by native_decide
1114
1115/-- μ(70) = -1 (squarefree with 3 prime factors). -/
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