chore(data/finsupp/pointwise): add missing finsupp.mul_zero_class (#…

…7049)
leanprover-community · Apr 6, 2021 · 6f38c14 · 6f38c14
1 parent aa665b1
commit 6f38c14
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/src/data/finsupp/pointwise.lean b/src/data/finsupp/pointwise.lean
@@ -46,6 +46,13 @@ begin
   apply h,
   cases w; { rw w, simp },
 end
+
+instance : mul_zero_class (α →₀ β) :=
+{ zero      := 0,
+  mul       := (*),
+  mul_zero  := λ f, by { ext, simp only [mul_apply, zero_apply, mul_zero], },
+  zero_mul  := λ f, by { ext, simp only [mul_apply, zero_apply, zero_mul], }, }
+
 end
 
 instance [semiring β] : semigroup (α →₀ β) :=