chore: add a couple of to_additives (#7535)

leanprover-community · Oct 6, 2023 · fb3884a · fb3884a
1 parent 8ec1ec7
commit fb3884a
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/Mathlib/Algebra/BigOperators/Multiset/Basic.lean b/Mathlib/Algebra/BigOperators/Multiset/Basic.lean
@@ -117,6 +117,7 @@ theorem prod_add (s t : Multiset α) : prod (s + t) = prod s * prod t :=
 #align multiset.prod_add Multiset.prod_add
 #align multiset.sum_add Multiset.sum_add
 
+@[to_additive]
 theorem prod_nsmul (m : Multiset α) : ∀ n : ℕ, (n • m).prod = m.prod ^ n
   | 0 => by
     rw [zero_nsmul, pow_zero]

diff --git a/Mathlib/Data/Finsupp/Multiset.lean b/Mathlib/Data/Finsupp/Multiset.lean
@@ -80,7 +80,7 @@ theorem toMultiset_map (f : α →₀ ℕ) (g : α → β) :
     rfl
 #align finsupp.to_multiset_map Finsupp.toMultiset_map
 
-@[simp]
+@[to_additive (attr := simp)]
 theorem prod_toMultiset [CommMonoid α] (f : α →₀ ℕ) :
     f.toMultiset.prod = f.prod fun a n => a ^ n := by
   refine' f.induction _ _