Commit 2021-07-20 10:51 fce38f1a

feat(ring_theory): define fractional_ideal.adjoin_integral (#8296) This PR shows if x is integral over R, then R[x] is a fractional ideal, and proves some of the essential properties of this fractional ideal. This is an important step towards showing is_dedekind_domain_inv implies that the ring is integrally closed. Co-Authored-By: Ashvni ashvni.n@gmail.com Co-Authored-By: Filippo A. E. Nuccio filippo.nuccio@univ-st-etienne.fr