Commit 2021-07-26 15:58 708b25d2
View on Github →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 [email protected]
Co-Authored-By: Filippo A. E. Nuccio [email protected]