From 3b194f9ac3503f4e91593d3250803c7f6a3d790c Mon Sep 17 00:00:00 2001 From: Seewoo Lee <49933279+seewoo5@users.noreply.github.com> Date: Wed, 30 Oct 2024 18:07:00 -0700 Subject: [PATCH] Update Mathlib/RingTheory/Radical.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- 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 5b96cb7664a72..d92fe352fef46 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) -theorem IsCoprime.divRadical {a b : E} (h : IsCoprime a b) : +protected theorem 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