Def EuclideanDomain.divRadical

Modification history

2024-10-31 18:17
Mathlib/RingTheory/Radical.lean
feat: dividing an element of a euclidean domain by its radical (#18449) …
Added EuclideanDomain.divRadicalView on Github →