mathlib3

cfecf720 - feat(algebra/module): push forward the action of `R` on `M` along `f : R → S` (#10502)

feat(algebra/module): push forward the action of `R` on `M` along `f : R → S` (#10502) If `f : R →+* S` is compatible with the `R`-module structure on `M`, and the scalar action of `S` on `M`, then `M` gets an `S`-module structure too. Additionally, if `R` is a ring and the kernel of `f` acts on `M` by sending it to `0`, then we don't need to specify the scalar action of `S` on `M` (but it is still possible for defeq purposes). These definitions should allow you to turn an action of `R` on `M` into an action of `R/I` on `M/N` via the (previously defined) action of `R` on `M/N`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>