use _root_ for IsCoprime.divRadical

leanprover-community · Oct 31, 2024 · 6105ab9 · 6105ab9
1 parent e9520ae
commit 6105ab9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/RingTheory/Radical.lean b/Mathlib/RingTheory/Radical.lean
@@ -218,7 +218,7 @@ theorem divRadical_mul {a b : E} (hab : IsCoprime a b) :
 theorem divRadical_dvd_self (a : E) : divRadical a ∣ a := by
   exact Dvd.intro (radical a) (divRadical_mul_radical a)
 
-protected theorem IsCoprime.divRadical {a b : E} (h : IsCoprime a b) :
+theorem _root_.IsCoprime.divRadical {a b : E} (h : IsCoprime a b) :
     IsCoprime (divRadical a) (divRadical b) := by
   rw [← radical_mul_divRadical a] at h
   rw [← radical_mul_divRadical b] at h