From d6c55bf6a8d29a968f217c0a705413a3c05aef2e Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 18 Apr 2026 18:27:03 +0800 Subject: [PATCH 1/2] refactor: golf only `FactorisationProperties` --- .../NumberTheory/FactorisationProperties.lean | 41 +++++-------------- 1 file changed, 11 insertions(+), 30 deletions(-) diff --git a/Mathlib/NumberTheory/FactorisationProperties.lean b/Mathlib/NumberTheory/FactorisationProperties.lean index 4f6abdecba6666..62ea986210d0f2 100644 --- a/Mathlib/NumberTheory/FactorisationProperties.lean +++ b/Mathlib/NumberTheory/FactorisationProperties.lean @@ -126,42 +126,23 @@ theorem Prime.not_weird (h : Prime n) : ¬ Weird n := by grind [Weird, h.not_abundant] theorem Prime.not_pseudoperfect (h : Prime p) : ¬ Pseudoperfect p := by - simp_rw [not_pseudoperfect_iff_forall, ← mem_powerset, - show p.properDivisors.powerset = {∅, {1}} by rw [Prime.properDivisors h]; rfl] - refine Or.inr (fun s hs ↦ ?_) - fin_cases hs <;> - simp only [sum_empty, sum_singleton] <;> - grind [Prime.one_lt h] - -theorem Prime.not_perfect (h : Prime p) : ¬ Perfect p := by - have h1 := Prime.not_pseudoperfect h - revert h1 - exact not_imp_not.mpr (Perfect.pseudoperfect) + rw [not_pseudoperfect_iff_forall] + refine Or.inr fun s hs => ne_of_lt (lt_of_le_of_lt ?_ h.one_lt) + rw [Prime.properDivisors h] at hs + simpa using Finset.sum_le_sum_of_subset hs + +theorem Prime.not_perfect (h : Prime p) : ¬ Perfect p := + fun hp ↦ h.not_pseudoperfect hp.pseudoperfect /-- Any natural number power of a prime is deficient -/ theorem Prime.deficient_pow (h : Prime n) : Deficient (n ^ m) := by rcases Nat.eq_zero_or_pos m with (rfl | _) · simpa using deficient_one - · have h1 : (n ^ m).properDivisors = image (n ^ ·) (range m) := by - apply subset_antisymm <;> intro a - · simp only [mem_properDivisors, mem_image, mem_range, dvd_prime_pow h] - rintro ⟨⟨t, ht, rfl⟩, ha'⟩ - exact ⟨t, lt_of_le_of_ne ht (fun ht' ↦ lt_irrefl _ (ht' ▸ ha')), rfl⟩ - · simp only [mem_image, mem_range, mem_properDivisors, forall_exists_index, and_imp] - intro x hx hy - constructor - · rw [← hy, dvd_prime_pow h] - exact ⟨x, Nat.le_of_succ_le hx, rfl⟩ - · rw [← hy] - exact (Nat.pow_lt_pow_iff_right (Prime.two_le h)).mpr hx - have h2 : ∑ i ∈ image (fun x => n ^ x) (range m), i = ∑ i ∈ range m, n ^ i := by - rw [sum_image] - rintro x _ y _ - apply pow_injective_of_not_isUnit h.not_isUnit <| Prime.ne_zero h - rw [Deficient, h1, h2] + · rw [Deficient, properDivisors_prime_pow h] calc - ∑ i ∈ range m, n ^ i - = (n ^ m - 1) / (n - 1) := (Nat.geomSum_eq (Prime.two_le h) _) + ∑ x ∈ Finset.map ⟨(n ^ ·), Nat.pow_right_injective h.two_le⟩ (range m), x + = ∑ i ∈ range m, n ^ i := by simp + _ = (n ^ m - 1) / (n - 1) := (Nat.geomSum_eq (Prime.two_le h) _) _ ≤ (n ^ m - 1) := Nat.div_le_self (n ^ m - 1) (n - 1) _ < n ^ m := sub_lt (pow_pos (Prime.pos h) m) (Nat.one_pos) From e6d37419e65e580702d9f93c26c9e2f4f8d07532 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sun, 19 Apr 2026 17:52:55 +0800 Subject: [PATCH 2/2] Apply suggestion from @MichaelStollBayreuth Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/FactorisationProperties.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/FactorisationProperties.lean b/Mathlib/NumberTheory/FactorisationProperties.lean index 62ea986210d0f2..00ed37e5c471c2 100644 --- a/Mathlib/NumberTheory/FactorisationProperties.lean +++ b/Mathlib/NumberTheory/FactorisationProperties.lean @@ -127,7 +127,7 @@ theorem Prime.not_weird (h : Prime n) : ¬ Weird n := by theorem Prime.not_pseudoperfect (h : Prime p) : ¬ Pseudoperfect p := by rw [not_pseudoperfect_iff_forall] - refine Or.inr fun s hs => ne_of_lt (lt_of_le_of_lt ?_ h.one_lt) + refine Or.inr fun s hs ↦ ne_of_lt (lt_of_le_of_lt ?_ h.one_lt) rw [Prime.properDivisors h] at hs simpa using Finset.sum_le_sum_of_subset hs