feat(Data/Nat/Squarefree): add divisors_filter_squarefree_of_squarefr…

…ee (#5835) Add a lemma that helps when applying `divisors_filter_squarefree` or `sum_divisors_filter_squarefree` in the case where `n` is squarefree.
leanprover-community · Jul 18, 2023 · 1c34db8 · 1c34db8
1 parent beb5b35
commit 1c34db8
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean
@@ -257,6 +257,11 @@ theorem squarefree_two : Squarefree 2 := by
   · norm_num
 #align nat.squarefree_two Nat.squarefree_two
 
+theorem divisors_filter_squarefree_of_squarefree {n : ℕ} (hn : Squarefree n) :
+    n.divisors.filter Squarefree = n.divisors :=
+  Finset.ext fun d => ⟨@Finset.filter_subset _ _ _ _ d, fun hd =>
+    Finset.mem_filter.mpr ⟨hd, hn.squarefree_of_dvd (Nat.dvd_of_mem_divisors hd) ⟩⟩
+
 open UniqueFactorizationMonoid
 
 theorem divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) :