mathlib

286d6750 - feat(algebra/category/Module/change_of_rings): restriction of scalars (#15672)

feat(algebra/category/Module/change_of_rings): restriction of scalars (#15672) Given a ring homomorphism $f : R\to S$, there is a functor from $S$-module to $R$-module. In #15564, it will proven that extension of scalars $\dashv$ restriction of scalars