mathlib

708b25d2 - feat(ring_theory): (fractional) ideals are finitely generated if they are invertible (#8294)

feat(ring_theory): (fractional) ideals are finitely generated if they are invertible (#8294) This is one of the three steps in showing `is_dedekind_domain_inv` implies `is_dedekind_domain`. Co-Authored-By: Ashvni ashvni.n@gmail.com Co-Authored-By: Filippo A. E. Nuccio filippo.nuccio@univ-st-etienne.fr Co-authored-by: Johan Commelin <johan@commelin.net>