feat(ring_theory/dedekind_domain): definitions (#4000)
Defines `is_dedekind_domain` in three variants:
1. `is_dedekind_domain`: Noetherian, Integrally closed, Krull dimension 1, thanks to @Vierkantor
2. `is_dedekind_domain_dvr`: Noetherian, localization at every nonzero prime is a DVR
3. `is_dedekind_domain_inv`: Every nonzero ideal is invertible.
TODO: prove that these definitions are equivalent.
This PR also includes some misc. lemmas required to show the definitions are independent of choice of fraction field.
Co-Authored-By: mushokunosora <knaka3435@gmail.com>
Co-Authored-By: faenuccio <filippo.nuccio@univ-st-etienne.fr>
Co-Authored-By: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Anne Baanen <t.baanen@vu.nl>
Co-authored-by: mushokunosora <38799099+mushokunosora@users.noreply.github.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
