Commit 2025-08-11 10:26 35f3847f
View on Github →feat(RingTheory/Finiteness): add Submodule.fg_iff_exists_fin_linearMap (#27957)
which generalizes Module.Finite.exists_fin'. Also clean up some unused universes/variables and simplify the proof of Module.Finite.exists_fin' using this new theorem.