mathlib

fce38f1a - feat(ring_theory): define `fractional_ideal.adjoin_integral` (#8296)

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