mathlib

9e274549 - feat(algebra/category/Module/change_of_rings): extension of scalars (#15673)

feat(algebra/category/Module/change_of_rings): extension of scalars (#15673) Given a ring homomorphism $f : R \to S$ between commutative rings, the extension of scalars functor from $R$-module to $S$-module. In #15564 it will proven that extension of scalars $\dashv$ restriction of scalars Co-authored-by: Jujian Zhang <jujian@192.168.1.104>