mathlib3

ea1dd3d3 - feat(algebra/module/localized_module): add characteristic predicate for `localized_module` (#15507)

feat(algebra/module/localized_module): add characteristic predicate for `localized_module` (#15507) Add characteristic predicate for localised module similar to ring localization and prove that the concrete construction satisfies the characteristic predicate. Co-authored-by: Andrew Yang @erdOne