mathlib3

5bac21a1 - 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.