Documentation

Mathlib.NumberTheory.ArithmeticFunction

Arithmetic Functions and Dirichlet Convolution #

This file defines arithmetic functions, which are functions from to a specified type that map 0 to 0. In the literature, they are often instead defined as functions from ℕ+. These arithmetic functions are endowed with a multiplication, given by Dirichlet convolution, and pointwise addition, to form the Dirichlet ring.

Main Definitions #

Main Results #

Notation #

All notation is localized in the namespace ArithmeticFunction.

The arithmetic functions ζ, σ, ω, Ω and μ have Greek letter names.

In addition, there are separate locales ArithmeticFunction.zeta for ζ, ArithmeticFunction.sigma for σ, ArithmeticFunction.omega for ω, ArithmeticFunction.Omega for Ω, and ArithmeticFunction.Moebius for μ, to allow for selective access to these notations.

The arithmetic function $$n \mapsto \prod_{p \mid n} f(p)$$ is given custom notation ∏ᵖ p ∣ n, f p when applied to n.

Tags #

arithmetic functions, dirichlet convolution, divisors

def ArithmeticFunction (R : Type u_1) [Zero R] :
Type (max 0 u_1)

An arithmetic function is a function from that maps 0 to 0. In the literature, they are often instead defined as functions from ℕ+. Multiplication on ArithmeticFunctions is by Dirichlet convolution.

Equations
Instances For
    Equations
    @[simp]
    theorem ArithmeticFunction.toFun_eq {R : Type u_1} [Zero R] (f : ArithmeticFunction R) :
    f.toFun = f
    @[simp]
    theorem ArithmeticFunction.coe_mk {R : Type u_1} [Zero R] (f : R) (hf : f 0 = 0) :
    { toFun := f, map_zero' := hf } = f
    @[simp]
    theorem ArithmeticFunction.map_zero {R : Type u_1} [Zero R] {f : ArithmeticFunction R} :
    f 0 = 0
    theorem ArithmeticFunction.coe_inj {R : Type u_1} [Zero R] {f : ArithmeticFunction R} {g : ArithmeticFunction R} :
    f = g f = g
    @[simp]
    theorem ArithmeticFunction.zero_apply {R : Type u_1} [Zero R] {x : } :
    0 x = 0
    theorem ArithmeticFunction.ext_iff {R : Type u_1} [Zero R] {f : ArithmeticFunction R} {g : ArithmeticFunction R} :
    f = g ∀ (x : ), f x = g x
    theorem ArithmeticFunction.ext {R : Type u_1} [Zero R] ⦃f : ArithmeticFunction R ⦃g : ArithmeticFunction R (h : ∀ (x : ), f x = g x) :
    f = g
    instance ArithmeticFunction.one {R : Type u_1} [Zero R] [One R] :
    Equations
    • ArithmeticFunction.one = { one := { toFun := fun (x : ) => if x = 1 then 1 else 0, map_zero' := } }
    theorem ArithmeticFunction.one_apply {R : Type u_1} [Zero R] [One R] {x : } :
    1 x = if x = 1 then 1 else 0
    @[simp]
    theorem ArithmeticFunction.one_one {R : Type u_1} [Zero R] [One R] :
    1 1 = 1
    @[simp]
    theorem ArithmeticFunction.one_apply_ne {R : Type u_1} [Zero R] [One R] {x : } (h : x 1) :
    1 x = 0

    Coerce an arithmetic function with values in to one with values in R. We cannot inline this in natCoe because it gets unfolded too much.

    Equations
    • f = { toFun := fun (n : ) => (f n), map_zero' := }
    Instances For
      Equations
      • ArithmeticFunction.natCoe = { coe := ArithmeticFunction.natToArithmeticFunction }
      @[simp]
      theorem ArithmeticFunction.natCoe_apply {R : Type u_1} [AddMonoidWithOne R] {f : ArithmeticFunction } {x : } :
      f x = (f x)

      Coerce an arithmetic function with values in to one with values in R. We cannot inline this in intCoe because it gets unfolded too much.

      Equations
      • f = { toFun := fun (n : ) => (f n), map_zero' := }
      Instances For
        Equations
        • ArithmeticFunction.intCoe = { coe := ArithmeticFunction.ofInt }
        @[simp]
        theorem ArithmeticFunction.intCoe_apply {R : Type u_1} [AddGroupWithOne R] {f : ArithmeticFunction } {x : } :
        f x = (f x)
        @[simp]
        theorem ArithmeticFunction.coe_coe {R : Type u_1} [AddGroupWithOne R] {f : ArithmeticFunction } :
        f = f
        @[simp]
        @[simp]
        theorem ArithmeticFunction.intCoe_one {R : Type u_1} [AddGroupWithOne R] :
        1 = 1
        Equations
        • ArithmeticFunction.add = { add := fun (f g : ArithmeticFunction R) => { toFun := fun (n : ) => f n + g n, map_zero' := } }
        @[simp]
        theorem ArithmeticFunction.add_apply {R : Type u_1} [AddMonoid R] {f : ArithmeticFunction R} {g : ArithmeticFunction R} {n : } :
        (f + g) n = f n + g n
        Equations
        • ArithmeticFunction.instAddMonoid = AddMonoid.mk nsmulRec
        Equations
        Equations
        Equations
        • ArithmeticFunction.instNeg = { neg := fun (f : ArithmeticFunction R) => { toFun := fun (n : ) => -f n, map_zero' := } }
        Equations
        Equations

        The Dirichlet convolution of two arithmetic functions f and g is another arithmetic function such that (f * g) n is the sum of f x * g y over all (x,y) such that x * y = n.

        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem ArithmeticFunction.smul_apply {R : Type u_1} {M : Type u_2} [Zero R] [AddCommMonoid M] [SMul R M] {f : ArithmeticFunction R} {g : ArithmeticFunction M} {n : } :
        (f g) n = xn.divisorsAntidiagonal, f x.1 g x.2

        The Dirichlet convolution of two arithmetic functions f and g is another arithmetic function such that (f * g) n is the sum of f x * g y over all (x,y) such that x * y = n.

        Equations
        @[simp]
        theorem ArithmeticFunction.mul_apply {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {g : ArithmeticFunction R} {n : } :
        (f * g) n = xn.divisorsAntidiagonal, f x.1 * g x.2
        theorem ArithmeticFunction.mul_apply_one {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {g : ArithmeticFunction R} :
        (f * g) 1 = f 1 * g 1
        @[simp]
        theorem ArithmeticFunction.natCoe_mul {R : Type u_1} [Semiring R] {f : ArithmeticFunction } {g : ArithmeticFunction } :
        (f * g) = f * g
        @[simp]
        theorem ArithmeticFunction.intCoe_mul {R : Type u_1} [Ring R] {f : ArithmeticFunction } {g : ArithmeticFunction } :
        (f * g) = f * g
        theorem ArithmeticFunction.mul_smul' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : ArithmeticFunction R) (g : ArithmeticFunction R) (h : ArithmeticFunction M) :
        (f * g) h = f g h
        theorem ArithmeticFunction.one_smul' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (b : ArithmeticFunction M) :
        1 b = b
        Equations
        • ArithmeticFunction.instMonoid = Monoid.mk npowRecAuto
        Equations
        • ArithmeticFunction.instSemiring = Semiring.mk Monoid.npow
        Equations
        Equations
        Equations

        ζ 0 = 0, otherwise ζ x = 1. The Dirichlet Series is the Riemann ζ.

        Equations
        Instances For

          ζ 0 = 0, otherwise ζ x = 1. The Dirichlet Series is the Riemann ζ.

          Equations
          Instances For

            ζ 0 = 0, otherwise ζ x = 1. The Dirichlet Series is the Riemann ζ.

            Equations
            Instances For
              @[simp]
              theorem ArithmeticFunction.zeta_apply {x : } :
              ArithmeticFunction.zeta x = if x = 0 then 0 else 1
              theorem ArithmeticFunction.zeta_apply_ne {x : } (h : x 0) :
              ArithmeticFunction.zeta x = 1
              theorem ArithmeticFunction.coe_zeta_smul_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {f : ArithmeticFunction M} {x : } :
              (ArithmeticFunction.zeta f) x = ix.divisors, f i
              theorem ArithmeticFunction.coe_zeta_mul_apply {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {x : } :
              (ArithmeticFunction.zeta * f) x = ix.divisors, f i
              theorem ArithmeticFunction.coe_mul_zeta_apply {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {x : } :
              (f * ArithmeticFunction.zeta) x = ix.divisors, f i
              theorem ArithmeticFunction.zeta_mul_apply {f : ArithmeticFunction } {x : } :
              (ArithmeticFunction.zeta * f) x = ix.divisors, f i
              theorem ArithmeticFunction.mul_zeta_apply {f : ArithmeticFunction } {x : } :
              (f * ArithmeticFunction.zeta) x = ix.divisors, f i

              This is the pointwise product of ArithmeticFunctions.

              Equations
              • f.pmul g = { toFun := fun (x : ) => f x * g x, map_zero' := }
              Instances For
                @[simp]
                theorem ArithmeticFunction.pmul_apply {R : Type u_1} [MulZeroClass R] {f : ArithmeticFunction R} {g : ArithmeticFunction R} {x : } :
                (f.pmul g) x = f x * g x
                theorem ArithmeticFunction.pmul_comm {R : Type u_1} [CommMonoidWithZero R] (f : ArithmeticFunction R) (g : ArithmeticFunction R) :
                f.pmul g = g.pmul f
                theorem ArithmeticFunction.pmul_assoc {R : Type u_1} [CommMonoidWithZero R] (f₁ : ArithmeticFunction R) (f₂ : ArithmeticFunction R) (f₃ : ArithmeticFunction R) :
                (f₁.pmul f₂).pmul f₃ = f₁.pmul (f₂.pmul f₃)

                This is the pointwise power of ArithmeticFunctions.

                Equations
                Instances For
                  @[simp]
                  theorem ArithmeticFunction.ppow_apply {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {k : } {x : } (kpos : 0 < k) :
                  (f.ppow k) x = f x ^ k
                  theorem ArithmeticFunction.ppow_succ' {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {k : } :
                  f.ppow (k + 1) = f.pmul (f.ppow k)
                  theorem ArithmeticFunction.ppow_succ {R : Type u_1} [Semiring R] {f : ArithmeticFunction R} {k : } {kpos : 0 < k} :
                  f.ppow (k + 1) = (f.ppow k).pmul f

                  This is the pointwise division of ArithmeticFunctions.

                  Equations
                  • f.pdiv g = { toFun := fun (n : ) => f n / g n, map_zero' := }
                  Instances For
                    @[simp]
                    theorem ArithmeticFunction.pdiv_apply {R : Type u_1} [GroupWithZero R] (f : ArithmeticFunction R) (g : ArithmeticFunction R) (n : ) :
                    (f.pdiv g) n = f n / g n
                    @[simp]

                    This result only holds for DivisionSemirings instead of GroupWithZeros because zeta takes values in ℕ, and hence the coercion requires an AddMonoidWithOne. TODO: Generalise zeta

                    The map $n \mapsto \prod_{p \mid n} f(p)$ as an arithmetic function

                    Equations
                    Instances For

                      ∏ᵖ p ∣ n, f p is custom notation for prodPrimeFactors f n

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem ArithmeticFunction.prodPrimeFactors_apply {R : Type u_1} [CommMonoidWithZero R] {f : R} {n : } (hn : n 0) :
                        (ArithmeticFunction.prodPrimeFactors fun (p : ) => f p) n = pn.primeFactors, f p

                        Multiplicative functions

                        Equations
                        • f.IsMultiplicative = (f 1 = 1 ∀ {m n : }, m.Coprime nf (m * n) = f m * f n)
                        Instances For
                          @[simp]
                          theorem ArithmeticFunction.IsMultiplicative.map_one {R : Type u_1} [MonoidWithZero R] {f : ArithmeticFunction R} (h : f.IsMultiplicative) :
                          f 1 = 1
                          @[simp]
                          theorem ArithmeticFunction.IsMultiplicative.map_mul_of_coprime {R : Type u_1} [MonoidWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {m : } {n : } (h : m.Coprime n) :
                          f (m * n) = f m * f n
                          theorem ArithmeticFunction.IsMultiplicative.map_prod {R : Type u_1} {ι : Type u_2} [CommMonoidWithZero R] (g : ι) {f : ArithmeticFunction R} (hf : f.IsMultiplicative) (s : Finset ι) (hs : (↑s).Pairwise (Nat.Coprime on g)) :
                          f (∏ is, g i) = is, f (g i)
                          theorem ArithmeticFunction.IsMultiplicative.map_prod_of_prime {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) (t : Finset ) (ht : pt, Nat.Prime p) :
                          f (∏ at, a) = at, f a
                          theorem ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) (l : ) (t : Finset ) (ht : t l.primeFactors) :
                          f (∏ at, a) = at, f a
                          theorem ArithmeticFunction.IsMultiplicative.natCast {R : Type u_1} {f : ArithmeticFunction } [Semiring R] (h : f.IsMultiplicative) :
                          (↑f).IsMultiplicative
                          @[deprecated ArithmeticFunction.IsMultiplicative.natCast]
                          theorem ArithmeticFunction.IsMultiplicative.nat_cast {R : Type u_1} {f : ArithmeticFunction } [Semiring R] (h : f.IsMultiplicative) :
                          (↑f).IsMultiplicative

                          Alias of ArithmeticFunction.IsMultiplicative.natCast.

                          theorem ArithmeticFunction.IsMultiplicative.intCast {R : Type u_1} {f : ArithmeticFunction } [Ring R] (h : f.IsMultiplicative) :
                          (↑f).IsMultiplicative
                          @[deprecated ArithmeticFunction.IsMultiplicative.intCast]
                          theorem ArithmeticFunction.IsMultiplicative.int_cast {R : Type u_1} {f : ArithmeticFunction } [Ring R] (h : f.IsMultiplicative) :
                          (↑f).IsMultiplicative

                          Alias of ArithmeticFunction.IsMultiplicative.intCast.

                          theorem ArithmeticFunction.IsMultiplicative.mul {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} {g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) :
                          (f * g).IsMultiplicative
                          theorem ArithmeticFunction.IsMultiplicative.pmul {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} {g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) :
                          (f.pmul g).IsMultiplicative
                          theorem ArithmeticFunction.IsMultiplicative.pdiv {R : Type u_1} [CommGroupWithZero R] {f : ArithmeticFunction R} {g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) :
                          (f.pdiv g).IsMultiplicative
                          theorem ArithmeticFunction.IsMultiplicative.multiplicative_factorization {R : Type u_1} [CommMonoidWithZero R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative) {n : } (hn : n 0) :
                          f n = n.factorization.prod fun (p k : ) => f (p ^ k)

                          For any multiplicative function f and any n > 0, we can evaluate f n by evaluating f at p ^ k over the factorization of n

                          theorem ArithmeticFunction.IsMultiplicative.iff_ne_zero {R : Type u_1} [MonoidWithZero R] {f : ArithmeticFunction R} :
                          f.IsMultiplicative f 1 = 1 ∀ {m n : }, m 0n 0m.Coprime nf (m * n) = f m * f n

                          A recapitulation of the definition of multiplicative that is simpler for proofs

                          theorem ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers {R : Type u_1} [CommMonoidWithZero R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative) (g : ArithmeticFunction R) (hg : g.IsMultiplicative) :
                          f = g ∀ (p i : ), Nat.Prime pf (p ^ i) = g (p ^ i)

                          Two multiplicative functions f and g are equal if and only if they agree on prime powers

                          theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_add_of_squarefree {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} {g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) {n : } (hn : Squarefree n) :
                          (ArithmeticFunction.prodPrimeFactors fun (p : ) => (f + g) p) n = (f * g) n
                          theorem ArithmeticFunction.IsMultiplicative.lcm_apply_mul_gcd_apply {R : Type u_1} [CommMonoidWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {x : } {y : } :
                          f (x.lcm y) * f (x.gcd y) = f x * f y

                          The identity on as an ArithmeticFunction.

                          Equations
                          Instances For
                            @[simp]
                            theorem ArithmeticFunction.id_apply {x : } :
                            ArithmeticFunction.id x = x

                            pow k n = n ^ k, except pow 0 0 = 0.

                            Equations
                            Instances For
                              @[simp]
                              theorem ArithmeticFunction.pow_apply {k : } {n : } :
                              (ArithmeticFunction.pow k) n = if k = 0 n = 0 then 0 else n ^ k

                              σ k n is the sum of the kth powers of the divisors of n

                              Equations
                              Instances For

                                σ k n is the sum of the kth powers of the divisors of n

                                Equations
                                Instances For

                                  σ k n is the sum of the kth powers of the divisors of n

                                  Equations
                                  Instances For
                                    theorem ArithmeticFunction.sigma_apply {k : } {n : } :
                                    (ArithmeticFunction.sigma k) n = dn.divisors, d ^ k
                                    theorem ArithmeticFunction.sigma_apply_prime_pow {k : } {p : } {i : } (hp : Nat.Prime p) :
                                    (ArithmeticFunction.sigma k) (p ^ i) = jFinset.range (i + 1), p ^ (j * k)
                                    theorem ArithmeticFunction.sigma_one_apply (n : ) :
                                    (ArithmeticFunction.sigma 1) n = dn.divisors, d
                                    theorem ArithmeticFunction.sigma_one_apply_prime_pow {p : } {i : } (hp : Nat.Prime p) :
                                    (ArithmeticFunction.sigma 1) (p ^ i) = kFinset.range (i + 1), p ^ k
                                    theorem ArithmeticFunction.IsMultiplicative.ppow {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {k : } :
                                    (f.ppow k).IsMultiplicative

                                    Ω n is the number of prime factors of n.

                                    Equations
                                    Instances For

                                      Ω n is the number of prime factors of n.

                                      Equations
                                      Instances For

                                        Ω n is the number of prime factors of n.

                                        Equations
                                        Instances For
                                          theorem ArithmeticFunction.cardFactors_apply {n : } :
                                          ArithmeticFunction.cardFactors n = n.primeFactorsList.length
                                          theorem ArithmeticFunction.cardFactors_zero :
                                          ArithmeticFunction.cardFactors 0 = 0
                                          @[simp]
                                          theorem ArithmeticFunction.cardFactors_one :
                                          ArithmeticFunction.cardFactors 1 = 0
                                          @[simp]
                                          theorem ArithmeticFunction.cardFactors_eq_one_iff_prime {n : } :
                                          ArithmeticFunction.cardFactors n = 1 Nat.Prime n
                                          theorem ArithmeticFunction.cardFactors_mul {m : } {n : } (m0 : m 0) (n0 : n 0) :
                                          ArithmeticFunction.cardFactors (m * n) = ArithmeticFunction.cardFactors m + ArithmeticFunction.cardFactors n
                                          theorem ArithmeticFunction.cardFactors_multiset_prod {s : Multiset } (h0 : s.prod 0) :
                                          ArithmeticFunction.cardFactors s.prod = (Multiset.map (⇑ArithmeticFunction.cardFactors) s).sum
                                          @[simp]
                                          theorem ArithmeticFunction.cardFactors_apply_prime {p : } (hp : Nat.Prime p) :
                                          ArithmeticFunction.cardFactors p = 1
                                          @[simp]
                                          theorem ArithmeticFunction.cardFactors_apply_prime_pow {p : } {k : } (hp : Nat.Prime p) :
                                          ArithmeticFunction.cardFactors (p ^ k) = k

                                          ω n is the number of distinct prime factors of n.

                                          Equations
                                          Instances For

                                            ω n is the number of distinct prime factors of n.

                                            Equations
                                            Instances For

                                              ω n is the number of distinct prime factors of n.

                                              Equations
                                              Instances For
                                                theorem ArithmeticFunction.cardDistinctFactors_zero :
                                                ArithmeticFunction.cardDistinctFactors 0 = 0
                                                @[simp]
                                                theorem ArithmeticFunction.cardDistinctFactors_one :
                                                ArithmeticFunction.cardDistinctFactors 1 = 0
                                                theorem ArithmeticFunction.cardDistinctFactors_apply {n : } :
                                                ArithmeticFunction.cardDistinctFactors n = n.primeFactorsList.dedup.length
                                                theorem ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree {n : } (h0 : n 0) :
                                                ArithmeticFunction.cardDistinctFactors n = ArithmeticFunction.cardFactors n Squarefree n
                                                @[simp]
                                                theorem ArithmeticFunction.cardDistinctFactors_apply_prime_pow {p : } {k : } (hp : Nat.Prime p) (hk : k 0) :
                                                ArithmeticFunction.cardDistinctFactors (p ^ k) = 1
                                                @[simp]
                                                theorem ArithmeticFunction.cardDistinctFactors_apply_prime {p : } (hp : Nat.Prime p) :
                                                ArithmeticFunction.cardDistinctFactors p = 1

                                                μ is the Möbius function. If n is squarefree with an even number of distinct prime factors, μ n = 1. If n is squarefree with an odd number of distinct prime factors, μ n = -1. If n is not squarefree, μ n = 0.

                                                Equations
                                                Instances For

                                                  μ is the Möbius function. If n is squarefree with an even number of distinct prime factors, μ n = 1. If n is squarefree with an odd number of distinct prime factors, μ n = -1. If n is not squarefree, μ n = 0.

                                                  Equations
                                                  Instances For

                                                    μ is the Möbius function. If n is squarefree with an even number of distinct prime factors, μ n = 1. If n is squarefree with an odd number of distinct prime factors, μ n = -1. If n is not squarefree, μ n = 0.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem ArithmeticFunction.moebius_apply_of_squarefree {n : } (h : Squarefree n) :
                                                      ArithmeticFunction.moebius n = (-1) ^ ArithmeticFunction.cardFactors n
                                                      @[simp]
                                                      theorem ArithmeticFunction.moebius_eq_zero_of_not_squarefree {n : } (h : ¬Squarefree n) :
                                                      ArithmeticFunction.moebius n = 0
                                                      theorem ArithmeticFunction.moebius_apply_one :
                                                      ArithmeticFunction.moebius 1 = 1
                                                      theorem ArithmeticFunction.moebius_ne_zero_iff_squarefree {n : } :
                                                      ArithmeticFunction.moebius n 0 Squarefree n
                                                      theorem ArithmeticFunction.moebius_eq_or (n : ) :
                                                      ArithmeticFunction.moebius n = 0 ArithmeticFunction.moebius n = 1 ArithmeticFunction.moebius n = -1
                                                      theorem ArithmeticFunction.moebius_ne_zero_iff_eq_or {n : } :
                                                      ArithmeticFunction.moebius n 0 ArithmeticFunction.moebius n = 1 ArithmeticFunction.moebius n = -1
                                                      theorem ArithmeticFunction.moebius_sq_eq_one_of_squarefree {l : } (hl : Squarefree l) :
                                                      ArithmeticFunction.moebius l ^ 2 = 1
                                                      theorem ArithmeticFunction.abs_moebius_eq_one_of_squarefree {l : } (hl : Squarefree l) :
                                                      |ArithmeticFunction.moebius l| = 1
                                                      theorem ArithmeticFunction.moebius_sq {n : } :
                                                      ArithmeticFunction.moebius n ^ 2 = if Squarefree n then 1 else 0
                                                      theorem ArithmeticFunction.abs_moebius {n : } :
                                                      |ArithmeticFunction.moebius n| = if Squarefree n then 1 else 0
                                                      theorem ArithmeticFunction.abs_moebius_le_one {n : } :
                                                      |ArithmeticFunction.moebius n| 1
                                                      theorem ArithmeticFunction.moebius_apply_prime {p : } (hp : Nat.Prime p) :
                                                      ArithmeticFunction.moebius p = -1
                                                      theorem ArithmeticFunction.moebius_apply_prime_pow {p : } {k : } (hp : Nat.Prime p) (hk : k 0) :
                                                      ArithmeticFunction.moebius (p ^ k) = if k = 1 then -1 else 0
                                                      theorem ArithmeticFunction.moebius_apply_isPrimePow_not_prime {n : } (hn : IsPrimePow n) (hn' : ¬Nat.Prime n) :
                                                      ArithmeticFunction.moebius n = 0
                                                      theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree {R : Type u_1} [CommSemiring R] {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) {n : } (hn : Squarefree n) :
                                                      pn.primeFactors, (1 + f p) = dn.divisors, f d
                                                      theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree {R : Type u_1} [CommRing R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative) {n : } (hn : Squarefree n) :
                                                      pn.primeFactors, (1 - f p) = dn.divisors, (ArithmeticFunction.moebius d) * f d
                                                      Equations
                                                      • ArithmeticFunction.instInvertibleNatToArithmeticFunctionZeta = { invOf := ArithmeticFunction.moebius, invOf_mul_self := , mul_invOf_self := }

                                                      A unit in ArithmeticFunction R that evaluates to ζ, with inverse μ.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem ArithmeticFunction.coe_zetaUnit {R : Type u_1} [CommRing R] :
                                                        ArithmeticFunction.zetaUnit = ArithmeticFunction.zeta
                                                        @[simp]
                                                        theorem ArithmeticFunction.inv_zetaUnit {R : Type u_1} [CommRing R] :
                                                        ArithmeticFunction.zetaUnit⁻¹ = ArithmeticFunction.moebius
                                                        theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq {R : Type u_1} [AddCommGroup R] {f : R} {g : R} :
                                                        (∀ n > 0, in.divisors, f i = g n) n > 0, xn.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 g x.2 = f n

                                                        Möbius inversion for functions to an AddCommGroup.

                                                        theorem ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq {R : Type u_1} [Ring R] {f : R} {g : R} :
                                                        (∀ n > 0, in.divisors, f i = g n) n > 0, xn.divisorsAntidiagonal, (ArithmeticFunction.moebius x.1) * g x.2 = f n

                                                        Möbius inversion for functions to a Ring.

                                                        theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq {R : Type u_1} [CommGroup R] {f : R} {g : R} :
                                                        (∀ n > 0, in.divisors, f i = g n) n > 0, xn.divisorsAntidiagonal, g x.2 ^ ArithmeticFunction.moebius x.1 = f n

                                                        Möbius inversion for functions to a CommGroup.

                                                        theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero {R : Type u_1} [CommGroupWithZero R] {f : R} {g : R} (hf : ∀ (n : ), 0 < nf n 0) (hg : ∀ (n : ), 0 < ng n 0) :
                                                        (∀ n > 0, in.divisors, f i = g n) n > 0, xn.divisorsAntidiagonal, g x.2 ^ ArithmeticFunction.moebius x.1 = f n

                                                        Möbius inversion for functions to a CommGroupWithZero.

                                                        theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on {R : Type u_1} [AddCommGroup R] {f : R} {g : R} (s : Set ) (hs : ∀ (m n : ), m nn sm s) :
                                                        (∀ n > 0, n sin.divisors, f i = g n) n > 0, n sxn.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 g x.2 = f n

                                                        Möbius inversion for functions to an AddCommGroup, where the equalities only hold on a well-behaved set.

                                                        theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on' {R : Type u_1} [AddCommGroup R] {f : R} {g : R} (s : Set ) (hs : ∀ (m n : ), m nn sm s) (hs₀ : 0s) :
                                                        (∀ ns, in.divisors, f i = g n) ns, xn.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 g x.2 = f n
                                                        theorem ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on {R : Type u_1} [Ring R] {f : R} {g : R} (s : Set ) (hs : ∀ (m n : ), m nn sm s) :
                                                        (∀ n > 0, n sin.divisors, f i = g n) n > 0, n sxn.divisorsAntidiagonal, (ArithmeticFunction.moebius x.1) * g x.2 = f n

                                                        Möbius inversion for functions to a Ring, where the equalities only hold on a well-behaved set.

                                                        theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on {R : Type u_1} [CommGroup R] {f : R} {g : R} (s : Set ) (hs : ∀ (m n : ), m nn sm s) :
                                                        (∀ n > 0, n sin.divisors, f i = g n) n > 0, n sxn.divisorsAntidiagonal, g x.2 ^ ArithmeticFunction.moebius x.1 = f n

                                                        Möbius inversion for functions to a CommGroup, where the equalities only hold on a well-behaved set.

                                                        theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero {R : Type u_1} [CommGroupWithZero R] (s : Set ) (hs : ∀ (m n : ), m nn sm s) {f : R} {g : R} (hf : n > 0, f n 0) (hg : n > 0, g n 0) :
                                                        (∀ n > 0, n sin.divisors, f i = g n) n > 0, n sxn.divisorsAntidiagonal, g x.2 ^ ArithmeticFunction.moebius x.1 = f n

                                                        Möbius inversion for functions to a CommGroupWithZero, where the equalities only hold on a well-behaved set.

                                                        theorem Nat.card_divisors {n : } (hn : n 0) :
                                                        n.divisors.card = xn.primeFactors, (n.factorization x + 1)
                                                        @[deprecated]
                                                        theorem ArithmeticFunction.card_divisors (n : ) (hn : n 0) :
                                                        n.divisors.card = xn.primeFactors, (n.factorization x + 1)
                                                        theorem Nat.sum_divisors {n : } (hn : n 0) :
                                                        dn.divisors, d = pn.primeFactors, kFinset.range (n.factorization p + 1), p ^ k
                                                        theorem Nat.Coprime.card_divisors_mul {m : } {n : } (hmn : m.Coprime n) :
                                                        (m * n).divisors.card = m.divisors.card * n.divisors.card
                                                        theorem Nat.Coprime.sum_divisors_mul {m : } {n : } (hmn : m.Coprime n) :
                                                        d(m * n).divisors, d = (∑ dm.divisors, d) * dn.divisors, d