feat(ring_theory): PIDs are Dedekind domains (#9063)
We had all the ingredients ready for a while, apparently I just forgot to PR the instance itself.
Co-Authored-By: Ashvni <ashvni.n@gmail.com>
Co-Authored-By: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
