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

liouville_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)

 300theorem liouville_prime {p : ℕ} (hp : Prime p) : liouville p = -1 := by

proof body

Term-mode proof.

 301  have hp' : Nat.Prime p := (prime_iff p).1 hp
 302  have hp_ne : p ≠ 0 := hp'.ne_zero
 303  simp only [liouville, hp_ne, ↓reduceIte, bigOmega]
 304  -- Ω(p) = 1 for prime p
 305  have hOmega : ArithmeticFunction.cardFactors p = 1 := ArithmeticFunction.cardFactors_apply_prime hp'
 306  rw [hOmega]
 307  norm_num
 308
 309/-- λ(p^k) = (-1)^k for prime p. -/

depends on (5)

Lean names referenced from this declaration's body.