chore: avoid Finset dependency in Algebra.Algebra.Defs (#16893)

Author: Ruben-VandeVelde

Mathlib/Algebra/Algebra/Basic.lean

@@ -522,3 +522,21 @@ lemma LinearEquiv.extendScalarsOfSurjective_symm (f : M ≃ₗ[R] N) :
     (f.extendScalarsOfSurjective h).symm = f.symm.extendScalarsOfSurjective h := rfl
 
 end surjective
+
+namespace algebraMap
+
+section CommSemiringCommSemiring
+
+variable {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A] {ι : Type*} {s : Finset ι}
+
+@[norm_cast]
+theorem coe_prod (a : ι → R) : (↑(∏ i ∈ s, a i : R) : A) = ∏ i ∈ s, (↑(a i) : A) :=
+  map_prod (algebraMap R A) a s
+
+@[norm_cast]
+theorem coe_sum (a : ι → R) : ↑(∑ i ∈ s, a i) = ∑ i ∈ s, (↑(a i) : A) :=
+  map_sum (algebraMap R A) a s
+
+end CommSemiringCommSemiring
+
+end algebraMap

Mathlib/Algebra/Algebra/Defs.lean

@@ -3,7 +3,6 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
-import Mathlib.Algebra.BigOperators.Group.Finset
 import Mathlib.Algebra.Module.LinearMap.Defs
 
 /-!
@@ -82,6 +81,7 @@ the second approach only when you need to weaken a condition on either `R` or `A
 -/
 
 assert_not_exists Field
+assert_not_exists Finset
 assert_not_exists Module.End
 
 universe u v w u₁ v₁
@@ -165,26 +165,6 @@ theorem coe_sub (a b : R) :
 
 end CommRingRing
 
-section CommSemiringCommSemiring
-
-variable {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
-
--- direct to_additive fails because of some mix-up with polynomials
-@[norm_cast]
-theorem coe_prod {ι : Type*} {s : Finset ι} (a : ι → R) :
-    (↑(∏ i ∈ s, a i : R) : A) = ∏ i ∈ s, (↑(a i) : A) :=
-  map_prod (algebraMap R A) a s
-
--- to_additive fails for some reason
-@[norm_cast]
-theorem coe_sum {ι : Type*} {s : Finset ι} (a : ι → R) :
-    ↑(∑ i ∈ s, a i) = ∑ i ∈ s, (↑(a i) : A) :=
-  map_sum (algebraMap R A) a s
-
--- Porting note: removed attribute [to_additive] coe_prod; why should this be a `to_additive`?
-
-end CommSemiringCommSemiring
-
 end algebraMap
 
 /-- Creating an algebra from a morphism to the center of a semiring. -/