Theorem EuclideanDomain.radical_mul_divRadical

Modification history

2025-06-01 19:52
Mathlib/RingTheory/Radical.lean
feat(RingTheory/Radical): generalise and fill in TODOs (#25335) …
Modified EuclideanDomain.radical_mul_divRadicalView on Github →
2024-10-31 18:17
Mathlib/RingTheory/Radical.lean
feat: dividing an element of a euclidean domain by its radical (#18449) …
Added EuclideanDomain.radical_mul_divRadicalView on Github →