minor generalizations

Mathlib/Algebra/MonoidAlgebra/Basic.lean

@@ -69,30 +69,30 @@ variable (k : Type u₁) (G : Type u₂) (H : Type*) {R : Type*}
 
 section
 
-variable [Semiring k]
-
 /-- The monoid algebra over a semiring `k` generated by the monoid `G`.
 It is the type of finite formal `k`-linear combinations of terms of `G`,
 endowed with the convolution product.
 -/
-def MonoidAlgebra : Type max u₁ u₂ :=
+def MonoidAlgebra [Zero k] : Type max u₁ u₂ :=
   G →₀ k
 #align monoid_algebra MonoidAlgebra
 
 -- Porting note: The compiler couldn't derive this.
-instance MonoidAlgebra.inhabited : Inhabited (MonoidAlgebra k G) :=
+instance MonoidAlgebra.inhabited [Zero k] : Inhabited (MonoidAlgebra k G) :=
   inferInstanceAs (Inhabited (G →₀ k))
 #align monoid_algebra.inhabited MonoidAlgebra.inhabited
 
 -- Porting note: The compiler couldn't derive this.
-instance MonoidAlgebra.addCommMonoid : AddCommMonoid (MonoidAlgebra k G) :=
+instance MonoidAlgebra.addCommMonoid [AddCommMonoid k] :
+    AddCommMonoid (MonoidAlgebra k G) :=
   inferInstanceAs (AddCommMonoid (G →₀ k))
 #align monoid_algebra.add_comm_monoid MonoidAlgebra.addCommMonoid
 
-instance MonoidAlgebra.instIsCancelAdd [IsCancelAdd k] : IsCancelAdd (MonoidAlgebra k G) :=
+instance MonoidAlgebra.instIsCancelAdd [AddCommMonoid k] [IsCancelAdd k] : IsCancelAdd (MonoidAlgebra k G) :=
   inferInstanceAs (IsCancelAdd (G →₀ k))
 
-instance MonoidAlgebra.coeFun : CoeFun (MonoidAlgebra k G) fun _ => G → k :=
+instance MonoidAlgebra.coeFun [AddCommMonoid k] :
+    CoeFun (MonoidAlgebra k G) fun _ => G → k :=
   Finsupp.instCoeFun
 #align monoid_algebra.has_coe_to_fun MonoidAlgebra.coeFun
 
@@ -104,7 +104,7 @@ variable {k G}
 
 section
 
-variable [Semiring k] [NonUnitalNonAssocSemiring R]
+variable [AddCommMonoid k] [NonUnitalNonAssocSemiring R]
 
 -- Porting note: `reducible` cannot be `local`, so we replace some definitions and theorems with
 --               new ones which have new types.
@@ -141,7 +141,7 @@ theorem mapDomain_sum {k' G' : Type*} [Semiring k'] {f : G → G'} {s : MonoidAl
   Finsupp.mapDomain_sum
 
 /-- A non-commutative version of `MonoidAlgebra.lift`: given an additive homomorphism `f : k →+ R`
-and a homomorphism `g : G → R`, returns the additive homomorphism from
+and a map `g : G → R`, returns the additive homomorphism from
 `MonoidAlgebra k G` such that `liftNC f g (single a b) = f b * g a`. If `f` is a ring homomorphism
 and the range of either `f` or `g` is in center of `R`, then the result is a ring homomorphism.  If
 `R` is a `k`-algebra and `f = algebraMap k R`, then the result is an algebra homomorphism called