Documentation

Mathlib.Data.Nat.Factorization.Induction

Induction principles involving factorizations #

Definitions #

def Nat.recOnPrimePow {P : Sort u_1} (h0 : P 0) (h1 : P 1) (h : (a p n : ) → Nat.Prime p¬p a0 < nP aP (p ^ n * a)) (a : ) :
P a

Given P 0, P 1 and a way to extend P a to P (p ^ n * a) for prime p not dividing a, we can define P for all natural numbers.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Nat.recOnPosPrimePosCoprime {P : Sort u_1} (hp : (p n : ) → Nat.Prime p0 < nP (p ^ n)) (h0 : P 0) (h1 : P 1) (h : (a b : ) → 1 < a1 < ba.Coprime bP aP bP (a * b)) (a : ) :
    P a

    Given P 0, P 1, and P (p ^ n) for positive prime powers, and a way to extend P a and P b to P (a * b) when a, b are positive coprime, we can define P for all natural numbers.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Nat.recOnPrimeCoprime {P : Sort u_1} (h0 : P 0) (hp : (p n : ) → Nat.Prime pP (p ^ n)) (h : (a b : ) → 1 < a1 < ba.Coprime bP aP bP (a * b)) (a : ) :
      P a

      Given P 0, P (p ^ n) for all prime powers, and a way to extend P a and P b to P (a * b) when a, b are positive coprime, we can define P for all natural numbers.

      Equations
      Instances For
        def Nat.recOnMul {P : Sort u_1} (h0 : P 0) (h1 : P 1) (hp : (p : ) → Nat.Prime pP p) (h : (a b : ) → P aP bP (a * b)) (a : ) :
        P a

        Given P 0, P 1, P p for all primes, and a way to extend P a and P b to P (a * b), we can define P for all natural numbers.

        Equations
        Instances For
          def Nat.recOnMul.hp'' {P : Sort u_1} (h1 : P 1) (hp : (p : ) → Nat.Prime pP p) (h : (a b : ) → P aP bP (a * b)) (p : ) (n : ) (hp' : Nat.Prime p) :
          P (p ^ n)

          The predicate holds on prime powers

          Equations
          Instances For
            theorem induction_on_primes {P : Prop} (h₀ : P 0) (h₁ : P 1) (h : ∀ (p a : ), Nat.Prime pP aP (p * a)) (n : ) :
            P n
            theorem Nat.prime_composite_induction {P : Prop} (zero : P 0) (one : P 1) (prime : ∀ (p : ), Nat.Prime pP p) (composite : ∀ (a : ), 2 aP a∀ (b : ), 2 bP bP (a * b)) (n : ) :
            P n

            Lemmas on multiplicative functions #

            theorem Nat.multiplicative_factorization {β : Type u_1} [CommMonoid β] (f : β) (h_mult : ∀ (x y : ), x.Coprime yf (x * y) = f x * f y) (hf : f 1 = 1) {n : } :
            n 0f n = n.factorization.prod fun (p k : ) => f (p ^ k)

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

            theorem Nat.multiplicative_factorization' {n : } {β : Type u_1} [CommMonoid β] (f : β) (h_mult : ∀ (x y : ), x.Coprime yf (x * y) = f x * f y) (hf0 : f 0 = 1) (hf1 : f 1 = 1) :
            f n = n.factorization.prod fun (p k : ) => f (p ^ k)

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