theorem proved term proof

`mobius_eighteen`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

1125theorem mobius_eighteen : mobius 18 = 0 := by native_decide

Term-mode proof.

1126
1127/-- μ(20) = 0 (not squarefree, 4 | 20). -/

Lean names referenced from this declaration's body.

mobius in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use