mathlib

fba86201 - feat(algebra/module/localized_module): construction of module localisation (#14470)

feat(algebra/module/localized_module): construction of module localisation (#14470) Give commutative ring $R$, multiplicative subset $S\subseteq R$ and an $R$-module $M$. We can localise $M$ by $S$ to be $$ \frac ms = \frac n t \iff \exists (u \in S), u(sn - tm) = 0 $$ This pr makes this construction and proves that the localised module is an $R_S$ module. Thanks @Vierkantor for substantial golfing.