chore: fix todo for sigmaFinsuppEquivDFinsupp_smul (#11355)

leanprover-community · Mar 14, 2024 · ac06536 · ac06536
1 parent 69adfea
commit ac06536
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/Mathlib/Data/Finsupp/ToDFinsupp.lean b/Mathlib/Data/Finsupp/ToDFinsupp.lean
@@ -355,12 +355,10 @@ def sigmaFinsuppAddEquivDFinsupp [AddZeroClass N] : ((Σi, η i) →₀ N) ≃+
 
 attribute [-instance] Finsupp.instAddZeroClass
 
---tofix: r • (sigma_finsupp_equiv_dfinsupp f) doesn't work.
 @[simp]
 theorem sigmaFinsuppEquivDFinsupp_smul {R} [Monoid R] [AddMonoid N] [DistribMulAction R N] (r : R)
-    (f : (Σi, η i) →₀ N) :
-    sigmaFinsuppEquivDFinsupp (r • f) =
-      @SMul.smul R (Π₀ i, η i →₀ N) MulAction.toSMul r (sigmaFinsuppEquivDFinsupp f) := by
+    (f : (Σ i, η i) →₀ N) :
+    sigmaFinsuppEquivDFinsupp (r • f) = r • sigmaFinsuppEquivDFinsupp f := by
   ext
   rfl
 #align sigma_finsupp_equiv_dfinsupp_smul sigmaFinsuppEquivDFinsupp_smul