Theorem EuclideanDomain.divRadical_mul_radical

Modification history

2025-06-01 19:52
Mathlib/RingTheory/Radical.lean
feat(RingTheory/Radical): generalise and fill in TODOs (#25335) …
Modified EuclideanDomain.divRadical_mul_radicalView 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.divRadical_mul_radicalView on Github →