mathlib3

ed90a7d3 - refactor(ring_theory): submodules that are units are finitely generated (#18510)

refactor(ring_theory): submodules that are units are finitely generated (#18510) + generalize from fractional_ideal to submodule. + the algebra doesn't have to be commutative. + introduce `fractional_ideal.coe_submodule_hom`. Potential future project: since we have [fractional_ideal.is_fractional_of_fg](https://leanprover-community.github.io/mathlib_docs/ring_theory/fractional_ideal.html#fractional_ideal.is_fractional_of_fg), submodules in a localization that are units are automatically fractional ideals, so [class_group](https://leanprover-community.github.io/mathlib_docs/ring_theory/class_group.html#class_group) could be defined as the invertible submodules in the fraction_ring modulo principal ones, without mentioning `is_fractional`. This might make `class_group` less complicated and therefore faster.