Commit 2026-01-11 14:20 344975b7
View on Github →chore: tidy results around Module.Finite (#33614)
In particular this replaces many chains of Module.finite_def and Submodule.fg_top with Module.Finite.iff_fg, or aliases for the forward and reverse implications.
This also golfs some FiniteDimensional results in terms of their Finite counterparts, and adds Submodule.fg_range as a shorthand for a common case of Submodule.fg_map.