mathlib

865ad478 - feat(algebra/module/pointwise_pi): add a file with lemmas on smul_pi (#9369)

feat(algebra/module/pointwise_pi): add a file with lemmas on smul_pi (#9369) Make a new file rather than add an import to either of `algebra.pointwise` or `algebra.module.pi`. From #2819