mathlib3

65b0c582 - feat(ring_theory/localization): some lemmas on `coe_submodule` (#8621)

feat(ring_theory/localization): some lemmas on `coe_submodule` (#8621) A small assortment of results on `is_localization.coe_submodule`, needed for elementary facts about the ideal class group.