Commit 2021-09-26 12:40 865ad478
View on Github →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
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