Dedekind psi function

DefinitionDedekind psi function#✓fully proved

The Dedekind psi function \(\psi\) is the arithmetic function with values in \(\mathbb{N}\) given by \(\psi(0) = 0\) and, for \(n > 0\),

\[ \psi(n) = \prod_{p^k \parallel n} p^{k-1} (p + 1), \]

the product running over the primes \(p\) dividing \(n\), with \(p^k\) the exact power of \(p\) dividing \(n\).

def dedekindPsi : ArithmeticFunction ℕ where
  toFun n := if n = 0 then 0 else n.factorization.prod fun p k => p ^ (k - 1) * (p + 1)
  map_zero' := by simp

Used by 5

Used byDedekind psi function as a product over prime powers · Product formula for the Dedekind psi function · Cleared-denominator product formula for the Dedekind psi function · Dedekind psi function at prime powers · Multiplicativity of the Dedekind psi function

TheoremDedekind psi function as a product over prime powers#✓fully proved

For every natural number \(n \ne 0\), the Dedekind psi function \(\psi\) satisfies

\[ \psi(n) = \prod_{p^k \parallel n} p^{k-1} (p + 1), \]

the product running over the primes \(p\) dividing \(n\), with \(p^k\) the exact power of \(p\) dividing \(n\).

theorem dedekindPsi_eq_prod_factorization {n : ℕ} (hn : n ≠ 0) :
    dedekindPsi n = n.factorization.prod fun p k => p ^ (k - 1) * (p + 1)

Uses 1 · Used by 3

Statement usesDedekind psi function

Used byCleared-denominator product formula for the Dedekind psi function · Dedekind psi function at prime powers · Multiplicativity of the Dedekind psi function

TheoremDedekind psi function at prime powers#✓fully proved

For every prime \(p\) and every natural number \(k > 0\), the Dedekind psi function \(\psi\) satisfies \(\psi(p^k) = p^{k-1} (p + 1)\).

theorem dedekindPsi_prime_pow {p k : ℕ} (hp : Nat.Prime p) (hk : 0 < k) :
    dedekindPsi (p ^ k) = p ^ (k - 1) * (p + 1)

Uses 2

Statement usesDedekind psi function

Proof usesDedekind psi function as a product over prime powers

TheoremMultiplicativity of the Dedekind psi function#✓fully proved

The Dedekind psi function \(\psi\) is multiplicative: \(\psi(1) = 1\) and \(\psi(mn) = \psi(m) \psi(n)\) for all coprime natural numbers \(m\) and \(n\).

theorem isMultiplicative_dedekindPsi : IsMultiplicative dedekindPsi

Uses 2

Statement usesDedekind psi function

Proof usesDedekind psi function as a product over prime powers

TheoremCleared-denominator product formula for the Dedekind psi function#✓fully proved

For every natural number \(n \ne 0\), the Dedekind psi function \(\psi\) satisfies

\[ \psi(n) \prod_{p \mid n} p = n \prod_{p \mid n} (p + 1), \]

both products running over the prime divisors \(p\) of \(n\).

theorem dedekindPsi_mul_prod_primeFactors {n : ℕ} (hn : n ≠ 0) :
    dedekindPsi n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p + 1)

Uses 2 · Used by 1

Statement usesDedekind psi function

Proof usesDedekind psi function as a product over prime powers

Used byProduct formula for the Dedekind psi function

TheoremProduct formula for the Dedekind psi function#✓fully proved

For every natural number \(n \ne 0\), the Dedekind psi function \(\psi\) satisfies, as an identity of rational numbers,

\[ \psi(n) = n \prod_{p \mid n} \Bigl(1 + \frac{1}{p}\Bigr), \]

the product running over the prime divisors \(p\) of \(n\).

theorem dedekindPsi_eq_rational_prod {n : ℕ} (hn : n ≠ 0) :
    (dedekindPsi n : ℚ) = (n : ℚ) * ∏ p ∈ n.primeFactors, (1 + (p : ℚ)⁻¹)

Uses 2

Statement usesDedekind psi function

Proof usesCleared-denominator product formula for the Dedekind psi function

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.