chore(algebra/module/pi): add `pi.smul_def` (#8311)
chore(algebra/module/pi): add `pi.smul_def` (#8311)

Sometimes it is useful to rewrite unapplied `s • x` (I need it in a branch that is not yet ready for review).

We already have `pi.zero_def`, `pi.add_def`, etc.







leanprover-community/mathlib,leanprover-community/mathlib