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.

Author: urkud

src/algebra/module/pi.lean

@@ -22,6 +22,7 @@ instance has_scalar {α : Type*} [Π i, has_scalar α $ f i] :
   has_scalar α (Π i : I, f i) :=
 ⟨λ s x, λ i, s • (x i)⟩
 
+lemma smul_def {α : Type*} [Π i, has_scalar α $ f i] (s : α) : s • x = λ i, s • x i := rfl
 @[simp] lemma smul_apply {α : Type*} [Π i, has_scalar α $ f i] (s : α) : (s • x) i = s • x i := rfl
 
 instance has_scalar' {g : I → Type*} [Π i, has_scalar (f i) (g i)] :