theorem
proved
term proof
liouville_prime_pow
show as:
view Lean formalization →
formal statement (Lean)
310theorem liouville_prime_pow {p k : ℕ} (hp : Prime p) :
311 liouville (p ^ k) = (-1) ^ k := by
proof body
Term-mode proof.
312 have hp' : Nat.Prime p := (prime_iff p).1 hp
313 cases k with
314 | zero => simp [liouville_one]
315 | succ k =>
316 have hpk : p ^ (k + 1) ≠ 0 := pow_ne_zero (k + 1) hp'.ne_zero
317 simp only [liouville, hpk, ↓reduceIte, bigOmega]
318 -- Ω(p^k) = k for prime p
319 have hOmega : ArithmeticFunction.cardFactors (p ^ (k + 1)) = k + 1 :=
320 ArithmeticFunction.cardFactors_apply_prime_pow hp'
321 rw [hOmega]
322
323/-- λ(mn) = λ(m) * λ(n) for nonzero m, n (complete multiplicativity). -/