pith. machine review for the scientific record. sign in
theorem proved term proof

mobius_eq_zero_iff_not_squarefree

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  50theorem mobius_eq_zero_iff_not_squarefree {n : ℕ} : mobius n = 0 ↔ ¬Squarefree n := by

proof body

Term-mode proof.

  51  -- Negate `μ n ≠ 0 ↔ Squarefree n`.
  52  simpa [not_ne_iff] using (not_congr (mobius_ne_zero_iff_squarefree (n := n)))
  53
  54/-- If `n` is squarefree then `μ n = (-1)^(cardFactors n)`. -/

depends on (6)

Lean names referenced from this declaration's body.