Documentation

Mathlib.Data.Nat.Factorization.Root

Roots of natural numbers, rounded up and down #

This file defines the flooring and ceiling root of a natural number. Nat.floorRoot n a/Nat.ceilRoot n a, the n-th flooring/ceiling root of a, is the natural number whose p-adic valuation is the floor/ceil of the p-adic valuation of a.

For example the 2-nd flooring and ceiling roots of 2^3 * 3^2 * 5 are 2 * 3 and 2^2 * 3 * 5 respectively. Note this is not the n-th root of a as a real number, rounded up or down.

These operations are respectively the right and left adjoints to the map a ↦ a ^ n where is ordered by divisibility. This is useful because it lets us characterise the numbers a whose n-th power divide n as the divisors of some fixed number (aka floorRoot n b). See Nat.pow_dvd_iff_dvd_floorRoot. Similarly, it lets us characterise the b whose n-th power is a multiple of a as the multiples of some fixed number (aka ceilRoot n a). See Nat.dvd_pow_iff_ceilRoot_dvd.

TODO #

def Nat.floorRoot (n : ) (a : ) :

Flooring root of a natural number. This divides the valuation of every prime number rounding down.

Eg if n = 2, a = 2^3 * 3^2 * 5, then floorRoot n a = 2 * 3.

In order theory terms, this is the upper or right adjoint of the map a ↦ a ^ n : ℕ → ℕ where is ordered by divisibility.

To ensure that the adjunction (Nat.pow_dvd_iff_dvd_floorRoot) holds in as many cases as possible, we special-case the following values:

Equations
Instances For
    theorem Nat.floorRoot_def {a : } {n : } :
    Nat.floorRoot n a = if n = 0 a = 0 then 0 else Finsupp.prod (Nat.factorization a ⌊/⌋ n) fun (x x_1 : ) => x ^ x_1

    The RHS is a noncomputable version of Nat.floorRoot with better order theoretical properties.

    @[simp]
    @[simp]
    @[simp]
    @[simp]
    theorem Nat.floorRoot_one_right {n : } (hn : n 0) :
    @[simp]
    theorem Nat.floorRoot_pow_self {n : } (hn : n 0) (a : ) :
    Nat.floorRoot n (a ^ n) = a
    theorem Nat.floorRoot_ne_zero {a : } {n : } :
    Nat.floorRoot n a 0 n 0 a 0
    @[simp]
    theorem Nat.floorRoot_eq_zero {a : } {n : } :
    Nat.floorRoot n a = 0 n = 0 a = 0
    theorem Nat.pow_dvd_iff_dvd_floorRoot {a : } {b : } {n : } :
    a ^ n b a Nat.floorRoot n b

    Galois connection between a ↦ a ^ n : ℕ → ℕ and floorRoot n : ℕ → ℕ where is ordered by divisibility.

    theorem Nat.floorRoot_pow_dvd {a : } {n : } :
    def Nat.ceilRoot (n : ) (a : ) :

    Ceiling root of a natural number. This divides the valuation of every prime number rounding up.

    Eg if n = 3, a = 2^4 * 3^2 * 5, then ceilRoot n a = 2^2 * 3 * 5.

    In order theory terms, this is the lower or left adjoint of the map a ↦ a ^ n : ℕ → ℕ where is ordered by divisibility.

    To ensure that the adjunction (Nat.dvd_pow_iff_ceilRoot_dvd) holds in as many cases as possible, we special-case the following values:

    Equations
    Instances For
      theorem Nat.ceilRoot_def {a : } {n : } :
      Nat.ceilRoot n a = if n = 0 a = 0 then 0 else Finsupp.prod (Nat.factorization a ⌈/⌉ n) fun (x x_1 : ) => x ^ x_1

      The RHS is a noncomputable version of Nat.ceilRoot with better order theoretical properties.

      @[simp]
      @[simp]
      @[simp]
      @[simp]
      theorem Nat.ceilRoot_one_right {n : } (hn : n 0) :
      @[simp]
      theorem Nat.ceilRoot_pow_self {n : } (hn : n 0) (a : ) :
      Nat.ceilRoot n (a ^ n) = a
      theorem Nat.ceilRoot_ne_zero {a : } {n : } :
      Nat.ceilRoot n a 0 n 0 a 0
      @[simp]
      theorem Nat.ceilRoot_eq_zero {a : } {n : } :
      Nat.ceilRoot n a = 0 n = 0 a = 0
      theorem Nat.dvd_pow_iff_ceilRoot_dvd {a : } {b : } {n : } (hn : n 0) :
      a b ^ n Nat.ceilRoot n a b

      Galois connection between ceilRoot n : ℕ → ℕ and a ↦ a ^ n : ℕ → ℕ where is ordered by divisibility.

      Note that this cannot possibly hold for n = 0, regardless of the value of ceilRoot 0 a, because the statement reduces to a = 1 ↔ ceilRoot 0 a ∣ b, which is false for eg a = 0, b = ceilRoot 0 a.

      theorem Nat.dvd_ceilRoot_pow {a : } {n : } (hn : n 0) :