chore(algebra/*): move function instances (#13650)

These should have been much earlier, but I put them in their current places to avoid large build times in what was an already large refactor.

src/algebra/algebra/basic.lean

@@ -1384,6 +1384,12 @@ rfl
 
 end pi
 
+/-- A special case of `pi.algebra` for non-dependent types. Lean struggles to elaborate
+definitions elsewhere in the library without this, -/
+instance function.algebra {R : Type*} (I : Type*)  (A : Type*) [comm_semiring R]
+  [semiring A] [algebra R A] : algebra R (I → A) :=
+pi.algebra _ _
+
 namespace alg_equiv
 
 /-- A family of algebra equivalences `Π j, (A₁ j ≃ₐ A₂ j)` generates a

src/geometry/manifold/algebra/smooth_functions.lean

@@ -233,12 +233,6 @@ instance algebra : algebra 𝕜 C^∞⟮I, N; 𝓘(𝕜, A), A⟯ :=
   smul_def' := λ c f, by ext x; exact algebra.smul_def' _ _,
   ..smooth_map.semiring }
 
-/-- A special case of `pi.algebra` for non-dependent types. Lean get stuck on the definition
-below without this. -/
-instance _root_.function.algebra (I : Type*) {R : Type*} (A : Type*) {r : comm_semiring R}
-  [semiring A] [algebra R A] : algebra R (I → A) :=
-pi.algebra _ _
-
 /-- Coercion to a function as an `alg_hom`. -/
 @[simps]
 def coe_fn_alg_hom : C^∞⟮I, N; 𝓘(𝕜, A), A⟯ →ₐ[𝕜] (N → A) :=

src/group_theory/group_action/pi.lean

@@ -154,6 +154,21 @@ end pi
 
 namespace function
 
+/-- Non-dependent version of `pi.has_scalar`. Lean gets confused by the dependent instance if this
+is not present. -/
+@[to_additive has_vadd]
+instance has_scalar {ι R M : Type*} [has_scalar R M] :
+  has_scalar R (ι → M) :=
+pi.has_scalar
+
+/-- Non-dependent version of `pi.smul_comm_class`. Lean gets confused by the dependent instance if
+this is not present. -/
+@[to_additive]
+instance smul_comm_class {ι α β M : Type*}
+  [has_scalar α M] [has_scalar β M] [smul_comm_class α β M] :
+  smul_comm_class α β (ι → M) :=
+pi.smul_comm_class
+
 @[to_additive]
 lemma update_smul {α : Type*} [Π i, has_scalar α (f i)] [decidable_eq I]
   (c : α) (f₁ : Π i, f i) (i : I) (x₁ : f i) :

src/linear_algebra/pi.lean

@@ -427,21 +427,6 @@ lemma linear_map.vec_cons_apply {n} (f : M →ₗ[R] M₂) (g : M →ₗ[R] (fin
 
 end semiring
 
-/-- Non-dependent version of `pi.has_scalar`. Lean gets confused by the dependent instance if this
-is not present. -/
-@[to_additive function.has_vadd]
-instance function.has_scalar {ι R M : Type*} [has_scalar R M] :
-  has_scalar R (ι → M) :=
-pi.has_scalar
-
-/-- Non-dependent version of `pi.smul_comm_class`. Lean gets confused by the dependent instance if
-this is not present. -/
-@[to_additive]
-instance function.smul_comm_class {ι α β M : Type*}
-  [has_scalar α M] [has_scalar β M] [smul_comm_class α β M]:
-  smul_comm_class α β (ι → M) :=
-pi.smul_comm_class
-
 section comm_semiring
 
 variables [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃]