MaxPrimeFac.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

21 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)

Imported by 1 file

FormalConjecturesForMathlib.lean

def Nat.maxPrimeFac The greatest prime divisor of a natural number n > 1 line 28 source
Source documentation
The greatest prime divisor of a natural number n > 1.
Takes the junk value 0 for n = 0 and 1 for n = 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: ite, Eq, OfNat.ofNat, List.getLastI, Nat.primeFactorsList
3 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def maxPrimeFac (n : ℕ) : ℕ := if n = 1 then 1 else n.primeFactorsList.getLastI
```
example Nat.(example at line 30) line 30 source
example Nat.(example at line 31) line 31 source
example Nat.(example at line 32) line 32 source
example Nat.(example at line 33) line 33 source
example Nat.(example at line 34) line 34 source
example Nat.(example at line 35) line 35 source
lemma Nat.maxPrimeFac_zero line 38 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Nat.maxPrimeFac, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite, List.getLastI, Nat.primeFactorsList, Inhabited.default, ite_cond_eq_false, List.nil, List, Nat.primeFactorsList_zero, List.getLastI.eq_1, eq_self
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Nat.maxPrimeFac_one line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Nat.maxPrimeFac, OfNat.ofNat
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma Nat.prime_maxPrimeFac_of_one_lt line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Nat.Prime, Nat.maxPrimeFac
Proof uses: Ne, List, Nat.primeFactorsList, List.nil, Iff.mpr, Nat.primeFactorsList_ne_nil, Membership.mem, List.getLast, List.getLast_mem, Nat.prime_of_mem_primeFactorsList, Eq.mpr, id, Eq, congrArg, Eq.trans, ite, List.getLastI, Option.getD, Option.some, ite_cond_eq_false and 8 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Nat.maxPrimeFac_dvd The greatest prime factor of a natural number divides it line 55 source
Source documentation
The greatest prime factor of a natural number divides it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, Nat.maxPrimeFac
Proof uses: Unit, of_eq_true, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, Nat.maxPrimeFac_zero, LT.lt, HAdd.hAdd, Decidable.byContradiction, Not, Ne, List, Nat.primeFactorsList, List.nil, Iff.mpr, Nat.primeFactorsList_ne_nil, Membership.mem, List.getLast and 17 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma maxPrimeFac_dvd : ∀ {n : ℕ}, maxPrimeFac n ∣ n
  | 0 => by simp
  | 1 => by simp
  | n + 2 => by
    have hn : 1 < n + 2 := by omega
…
```
Mentions: Nat.maxPrimeFac
lemma Nat.le_maxPrimeFac Every prime factor of a nonzero natural number is at most its greatest prime factor line 70 source
Source documentation
Every prime factor of a nonzero natural number is at most its greatest prime factor.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Nat.Prime, Dvd.dvd, LE.le, Nat.maxPrimeFac
Proof uses: Membership.mem, List, Nat.primeFactorsList, Iff.mpr, And, Nat.mem_primeFactorsList, And.intro, List.nil, List.ne_nil_of_mem, LT.lt.ne', Iff.mp, LT.lt, Nat.primeFactorsList_ne_nil, List.getLast, List.Pairwise.rel_getLast, List.SortedLE.pairwise, Nat.primeFactorsList_sorted, Eq.mpr, id, Eq and 14 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma le_maxPrimeFac
    {n p : ℕ} (hn : n ≠ 0) (hp : p.Prime) (h_dvd : p ∣ n) :
    p ≤ maxPrimeFac n := by
…
```
Mentions: Nat.maxPrimeFac
lemma Nat.maxPrimeFac_eq_of_dvd_of_le line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Nat.Prime, Dvd.dvd, LE.le, Nat.maxPrimeFac, Eq
Proof uses: le_antisymm, Nat.le_maxPrimeFac, LT.lt.ne'
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Nat.Prime.maxPrimeFac_eq_self The greatest prime factor of a prime is the prime itself line 88 source
Source documentation
The greatest prime factor of a prime is the prime itself.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Eq, Nat.maxPrimeFac
Proof uses: Nat.maxPrimeFac_eq_of_dvd_of_le, Nat.Prime.pos, dvd_refl, Nat.le_of_dvd, Nat.maxPrimeFac_dvd
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma Prime.maxPrimeFac_eq_self {p : ℕ} (hp : p.Prime) :
    maxPrimeFac p = p := by
…
```
Mentions: Nat.maxPrimeFac
lemma Nat.maxPrimeFac_eq_self_iff The fixed points of maxPrimeFac are zero, one, and the primes line 95 source
Source documentation
The fixed points of maxPrimeFac are zero, one, and the primes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Eq, Nat.maxPrimeFac, Or, LE.le, OfNat.ofNat, Nat.Prime
Proof uses: Iff.intro, dite, Or.inl, Not, Or.inr, Eq.rec, Nat.prime_maxPrimeFac_of_one_lt, lt_of_not_ge, Iff.mp, Nat.le_one_iff_eq_zero_or_eq_one, of_eq_true, Eq.trans, True, congrFun', congrArg, Nat.maxPrimeFac_zero, eq_self, Eq.symm, Nat.Prime.maxPrimeFac_eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma maxPrimeFac_eq_self_iff {n : ℕ} :
    maxPrimeFac n = n ↔ n ≤ 1 ∨ n.Prime := by
…
```
Mentions: Nat.maxPrimeFac
lemma Nat.maxPrimeFac_mul The greatest prime factor of a product of nonzero natural numbers is the maximum of their greatest prime factors line 108 source
Source documentation
The greatest prime factor of a product of nonzero natural numbers is the maximum of their greatest prime factors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Eq, Nat.maxPrimeFac, HMul.hMul, Max.max
Proof uses: LT.lt, Or, Decidable.byContradiction, Not, LE.le, of_eq_true, Eq.symm, LT.lt.le, Nat.Prime.one_lt, Nat.prime_maxPrimeFac_of_one_lt, Eq.trans, True, congr, congrArg, one_mul, sup_of_le_right, eq_self, mul_one, sup_of_le_left, Iff.mpr and 19 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma maxPrimeFac_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
    maxPrimeFac (m * n) = max (maxPrimeFac m) (maxPrimeFac n) := by
…
```
Mentions: Nat.maxPrimeFac
lemma Nat.maxPrimeFac_pow The greatest prime factor of a nonzero power is the greatest prime factor of its base line 136 source
Source documentation
The greatest prime factor of a nonzero power is the greatest prime factor of its base.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Eq, Nat.maxPrimeFac, HPow.hPow
Proof uses: HAdd.hAdd, dite, of_eq_true, Eq.trans, True, congr, congrArg, zero_pow, Not, False, And, and_false, not_false_eq_true, Nat.maxPrimeFac_zero, eq_self, Eq.symm, Nat.recAux, congrFun', zero_add, pow_one and 8 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma maxPrimeFac_pow {k : ℕ} (hk : k ≠ 0) (n : ℕ) :
    maxPrimeFac (n ^ k) = maxPrimeFac n :=
…
```
Mentions: Nat.maxPrimeFac
lemma Nat.maxPrimeFac_le The greatest prime factor of a natural number is at most that number line 150 source
Source documentation
The greatest prime factor of a natural number is at most that number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Nat.maxPrimeFac
Proof uses: Unit, of_eq_true, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, Nat.maxPrimeFac_zero, Nat.le_of_dvd, HAdd.hAdd, Decidable.byContradiction, LT.lt, Not, Nat.maxPrimeFac_dvd
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma maxPrimeFac_le : ∀ {n : ℕ}, maxPrimeFac n ≤ n
  | 0 => by simp
  | 1 => by simp
  | n + 2 => Nat.le_of_dvd (by omega) maxPrimeFac_dvd

/-- The greatest prime factor of a natural number greater than one is the least upper bound of
its prime factors. -/
```
Mentions: Nat.maxPrimeFac, Nat.maxPrimeFac_dvd
lemma Nat.isLeast_maxPrimeFac The greatest prime factor of a natural number greater than one is the least upper bound of its prime factors line 157 source
Source documentation
The greatest prime factor of a natural number greater than one is the least upper bound of its prime factors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, IsLeast, upperBounds, Set.ofPred, And, Nat.Prime, Dvd.dvd, Nat.maxPrimeFac
Proof uses: And.intro, Membership.mem, Set, lowerBounds, LE.le, Nat.le_maxPrimeFac, LT.lt.ne', Nat.zero_lt_of_lt, Nat.prime_maxPrimeFac_of_one_lt, Nat.maxPrimeFac_dvd
11 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma isLeast_maxPrimeFac {n : ℕ} (hn : 1 < n) :
    IsLeast (upperBounds {p : ℕ | p.Prime ∧ p ∣ n}) (maxPrimeFac n) := by
…
```
Mentions: Nat.maxPrimeFac
lemma Nat.maxPrimeFac_eq_sSup Away from n = 1, the computable greatest prime factor agrees with its supremum characterization line 167 source
Source documentation
Away from n = 1, the computable greatest prime factor agrees with its supremum characterization.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Eq, Nat.maxPrimeFac, SupSet.sSup, Set.ofPred, And, Nat.Prime, Dvd.dvd
Proof uses: LT.lt, Or, Eq.mpr, id, congr, congrArg, Nat.maxPrimeFac_zero, Set, funext, Eq.trans, True, and_true, Eq.symm, Set.Infinite.Nat.sSup_eq_zero, Nat.infinite_setOfPred_prime, IsLUB, Nat.isLeast_maxPrimeFac, IsLUB.csSup_eq, Exists.intro, Membership.mem and 3 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma maxPrimeFac_eq_sSup {n : ℕ} (hn_one : n ≠ 1) :
    maxPrimeFac n = sSup {p : ℕ | p.Prime ∧ p ∣ n} := by
…
```
Mentions: Nat.maxPrimeFac
lemma Nat.one_lt_maxPrimeFac_iff line 177 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, LT.lt, OfNat.ofNat, Nat.maxPrimeFac
Proof uses: Or, Eq, lt_trichotomy, of_eq_true, Eq.trans, False, True, congr, congrArg, Eq.mp, Nat.maxPrimeFac_zero, iff_self, Eq.symm, Eq.mpr, id, eq_true, iff_true, Nat.Prime.one_lt, Nat.prime_maxPrimeFac_of_one_lt
14 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.