Commit 2022-09-30 23:37 aa701d8f

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