mathlib

aa701d8f - feat(algebra/module/localized_module): universal property of localized module (#15559)

feat(algebra/module/localized_module): universal property of localized module (#15559) as $R$ module. `is_localized_module` also characterises localized module upto isomorphism as $R\_S$ module, this can be found in #16084 Co-authored-by: Andrew yang @erdOne