Skip to content

Commit

Permalink
Update Mathlib/RingTheory/Radical.lean
Browse files Browse the repository at this point in the history
Co-authored-by: Yaël Dillies <[email protected]>
  • Loading branch information
seewoo5 and YaelDillies authored Oct 31, 2024
1 parent 1d43d99 commit 3b194f9
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/RingTheory/Radical.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 3b194f9

Please sign in to comment.