fix(algebra/big_operators): change name of sum_attach to `finset.su…

…m_attach`
leanprover-community · Sep 7, 2018 · 2524dba · 2524dba
1 parent 8f89324
commit 2524dba
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/algebra/big_operators.lean b/algebra/big_operators.lean
@@ -150,7 +150,7 @@ from classical.by_cases
     calc s.prod f = (∅ : finset α).prod f : (prod_subset (empty_subset s) $ by simpa).symm
       ... = f a : (h₁ ‹a ∉ s›).symm)
 
-@[to_additive sum_attach]
+@[to_additive finset.sum_attach]
 lemma prod_attach {f : α → β} : s.attach.prod (λx, f x.val) = s.prod f :=
 by haveI := classical.dec_eq α; exact
 calc s.attach.prod (λx, f x.val) = ((s.attach).image subtype.val).prod f :