Commit 2021-07-13 16:48 8be0eda2

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