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

mobius_prime

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)

  29theorem mobius_prime {p : ℕ} (hp : Prime p) : (mobius p) = -1 := by

proof body

Term-mode proof.

  30  -- Mathlib lemma is `ArithmeticFunction.moebius_apply_prime` with `Nat.Prime`.
  31  have hp' : Nat.Prime p := (prime_iff p).1 hp
  32  simpa [mobius] using (ArithmeticFunction.moebius_apply_prime hp')
  33
  34/-- Möbius at a prime square: `μ(p^2) = 0`. -/

depends on (7)

Lean names referenced from this declaration's body.