chore(ring_theory): allow Dedekind domains to be fields (#8271)
During the Dedekind domain project, we found that the `¬ is_field R` condition is almost never needed, and it gets in the way when proving rings of integers are Dedekind domains. This PR removes this assumption from the three definitions.
Co-Authored-By: Ashvni <ashvni.n@gmail.com>
Co-Authored-By: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
