simp[HSMul.hSMul,SMul.smul]
Cont : Type u_3
Idx : outParam (Type u_4)
Elem : outParam (Type u_2)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
R : Type u_1
inst✝ : SMul R Elem
r : R
x : Cont
i : Idx
⊢ (r • x)[i] = r • x[i]
no goals