From 6105ab90ff1d02eb4aa6b9e5ec8dc1e22d4380ae Mon Sep 17 00:00:00 2001 From: Seewoo Lee Date: Thu, 31 Oct 2024 11:01:16 -0700 Subject: [PATCH] use _root_ for IsCoprime.divRadical --- Mathlib/RingTheory/Radical.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Radical.lean b/Mathlib/RingTheory/Radical.lean index b16f0360d9316..93460875b0a7c 100644 --- 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