Mathlib v3 is deprecated. Go to Mathlib v4

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 ashvni.n@gmail.com Co-Authored-By: Filippo A. E. Nuccio filippo.nuccio@univ-st-etienne.fr

Estimated changes