liouville_prime_pow

formal source

 307  norm_num
 308
 309/-- λ(p^k) = (-1)^k for prime p. -/
 310theorem liouville_prime_pow {p k : ℕ} (hp : Prime p) :
 311    liouville (p ^ k) = (-1) ^ k := by
 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). -/
 324theorem liouville_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
 325    liouville (m * n) = liouville m * liouville n := by
 326  have hmn : m * n ≠ 0 := mul_ne_zero hm hn
 327  simp only [liouville, hm, hn, hmn, ↓reduceIte]
 328  rw [bigOmega_mul hm hn, pow_add]
 329
 330/-! ### Identity function (for Dirichlet algebra) -/
 331
 332/-- The identity arithmetic function id(n) = n. -/
 333abbrev arithId : ArithmeticFunction ℕ := ArithmeticFunction.id
 334
 335@[simp] theorem arithId_def : arithId = ArithmeticFunction.id := rfl
 336
 337/-- id(n) = n. -/
 338theorem arithId_apply {n : ℕ} : arithId n = n := by
 339  simp [arithId]
 340