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

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

Takes the junk value 0 for n = 0 and n = 1.

TODO Consider redefining this using the computable implementation: n.primeFactorsList.getLastI.

Equations

• n.maxPrimeFac = sSup {p : ℕ | Nat.Prime p ∧ p ∣ n}

@[simp]

theorem Nat.maxPrimeFac_zero : maxPrimeFac 0 = 0

@[simp]

theorem Nat.maxPrimeFac_one : maxPrimeFac 1 = 0

theorem Nat.prime_maxPrimeFac_of_one_lt (n : ℕ) (h : 1 < n) : Prime n.maxPrimeFac

theorem Nat.maxPrimeFac_eq_of_dvd_of_le (n p : ℕ) (hn : 0 < n) (hp : Prime p) (h_dvd : p ∣ n) (h_le : n.maxPrimeFac ≤ p) : n.maxPrimeFac = p

@[simp]

theorem Nat.one_lt_maxPrimeFac_iff (n : ℕ) : 1 < n.maxPrimeFac ↔ 1 < n