mathlib3

190d4e28 - feat(algebra/module/basic): smul_add_hom_one (#7461)