chore(RepresentationTheory): drop some useless commutativity argument (#38117)

Author: Whysoserioushah

Mathlib/RepresentationTheory/Rep/Basic.lean

@@ -559,7 +559,9 @@ end Action
 
 end ring
 
-variable {k : Type u} {G : Type v} [CommRing k] [Monoid G]
+section CommSemiring
+
+variable {k : Type u} {G : Type v} [CommSemiring k] [Monoid G]
 
 instance {M N : Rep k G} : SMul k (M ⟶ N) where
   smul r f := ofHom (r • f.hom)
@@ -587,6 +589,10 @@ instance : Linear k (Rep k G) where
   smul_comp _ _ _ := smul_comp
   comp_smul _ _ _ := comp_smul
 
+end CommSemiring
+
+variable {k : Type u} {G : Type v} [CommRing k] [Monoid G]
+
 set_option backward.isDefEq.respectTransparency false in
 instance : Functor.Linear k (forget₂ (Rep.{w} k G) (ModuleCat.{w} k)) where
   map_smul {X Y} f r := by

Mathlib/RepresentationTheory/Rep/Res.lean

@@ -19,7 +19,7 @@ Given a group homomorphism `f : H →* G`, we have the restriction functor
 
 universe t w u v v1 v2
 
-variable {k : Type u} [CommRing k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H]
+variable {k : Type u} [Semiring k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H]
 
 open CategoryTheory
 
@@ -72,7 +72,7 @@ instance : (resFunctor (k := k) f).Additive where
     simp only [add_hom, Representation.IntertwiningMap.add_toLinearMap]
     rfl
 
-instance : (resFunctor (k := k) f).Linear k where
+instance {k : Type u} [CommSemiring k] : (resFunctor (k := k) f).Linear k where
   map_smul {X Y} l r := by
     ext : 2;
     rw [smul_hom, Representation.IntertwiningMap.toLinearMap_smul,