Documentation

Mathlib.Data.Nat.MaxPrimeFac

Greatest prime factor of a natural number #

This file defines Nat.maxPrimeFac, the greatest prime factor of a natural number greater than one, with explicit values at zero and one.

Implementation notes #

The list n.primeFactorsList is empty exactly when n = 0 or n = 1. We choose the junk values maxPrimeFac 0 = 0 and maxPrimeFac 1 = 1 so that:

Choosing maxPrimeFac 1 = 0 instead would make IsLUB {p : ℕ | p.Prime ∧ p ∣ n} (maxPrimeFac n) (but not IsGreatest {p : ℕ | p.Prime ∧ p ∣ n} (maxPrimeFac n)) hold for all n ≠ 0 and would make maxPrimeFac_eq_sSup hold unconditionally thanks to the junk value sSup ∅ = 0 on ℕ.

source
def Nat.maxPrimeFac (n : ℕ) :
ℕ

The greatest prime divisor of a natural number n > 1.

At the exceptional inputs n = 0 and n = 1, it returns the explicit default n because n.primeFactorsList is empty.

Equations
Instances For
    source
    @[simp]
    theorem Nat.maxPrimeFac_zero :
    maxPrimeFac 0 = 0
    source
    @[simp]
    theorem Nat.maxPrimeFac_one :
    maxPrimeFac 1 = 1
    source
    theorem Nat.prime_maxPrimeFac_of_one_lt {n : ℕ} (h : 1 < n) :
    Prime n.maxPrimeFac
    source
    theorem Nat.maxPrimeFac_dvd {n : ℕ} :
    n.maxPrimeFac ∣ n

    The greatest prime factor of a natural number divides it.

    source
    theorem Nat.le_maxPrimeFac {n p : ℕ} (hn : n ≠ 0) (hp : Prime p) (h_dvd : p ∣ n) :
    p ≤ n.maxPrimeFac

    Every prime factor of a nonzero natural number is at most its greatest prime factor.

    source
    theorem Nat.isGreatest_maxPrimeFac {n : ℕ} (hn : 1 < n) :
    IsGreatest {p : ℕ | Prime p ∧ p ∣ n} n.maxPrimeFac

    The greatest prime factor of a natural number greater than one is the greatest of its prime factors.

    source
    theorem Nat.isLUB_maxPrimeFac {n : ℕ} (hn : 1 < n) :
    IsLUB {p : ℕ | Prime p ∧ p ∣ n} n.maxPrimeFac

    The greatest prime factor of a natural number greater than one is the least upper bound of its prime factors.

    source
    theorem Nat.maxPrimeFac_le_iff {m n : ℕ} (hn : 1 < n) :
    n.maxPrimeFac ≤ m ↔ ∀ (p : ℕ), Prime p → p ∣ n → p ≤ m
    source
    @[simp]
    theorem Nat.one_le_maxPrimeFac_iff {n : ℕ} :
    1 ≤ n.maxPrimeFac ↔ 1 ≤ n
    source
    @[simp]
    theorem Nat.one_lt_maxPrimeFac_iff {n : ℕ} :
    1 < n.maxPrimeFac ↔ 1 < n
    source
    theorem Nat.maxPrimeFac_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
    (m * n).maxPrimeFac = max m.maxPrimeFac n.maxPrimeFac

    The greatest prime factor of a product of nonzero natural numbers is the maximum of their greatest prime factors.

    source
    @[simp]
    theorem Nat.maxPrimeFac_pow {k : ℕ} :
    k ≠ 0 → ∀ (n : ℕ), (n ^ k).maxPrimeFac = n.maxPrimeFac

    The greatest prime factor of a power with nonzero exponent is the greatest prime factor of its base.

    source
    @[simp]
    theorem Nat.Prime.maxPrimeFac_eq_self {p : ℕ} (hp : Prime p) :
    p.maxPrimeFac = p

    The greatest prime factor of a prime is the prime itself.

    source
    @[simp]
    theorem Nat.maxPrimeFac_eq_self_iff {n : ℕ} :
    n.maxPrimeFac = n ↔ n ≤ 1 ∨ Prime n

    The fixed points of maxPrimeFac are zero, one, and the primes.

    source
    theorem Nat.maxPrimeFac_le {n : ℕ} :
    n.maxPrimeFac ≤ n

    The greatest prime factor of a natural number is at most that number.

    source
    theorem Nat.maxPrimeFac_eq_sSup {n : ℕ} (hn_one : n ≠ 1) :
    n.maxPrimeFac = sSup {p : ℕ | Prime p ∧ p ∣ n}

    Away from n = 1, the computable greatest prime factor agrees with its supremum characterization.