chore(linear_algebra/basic): generalize add_monoid_hom_lequiv_{nat,int} (#9233)

Author: eric-wieser

src/linear_algebra/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
 -/
 import algebra.big_operators.pi
+import algebra.module.hom
 import algebra.module.prod
 import algebra.module.submodule_lattice
 import data.dfinsupp
@@ -635,11 +636,12 @@ end comm_ring
 end linear_map
 
 /--
-The `ℕ`-linear equivalence between additive morphisms `A →+ B` and `ℕ`-linear morphisms `A →ₗ[ℕ] B`.
+The `R`-linear equivalence between additive morphisms `A →+ B` and `ℕ`-linear morphisms `A →ₗ[ℕ] B`.
 -/
 @[simps]
-def add_monoid_hom_lequiv_nat {A B : Type*} [add_comm_monoid A] [add_comm_monoid B] :
-  (A →+ B) ≃ₗ[ℕ] (A →ₗ[ℕ] B) :=
+def add_monoid_hom_lequiv_nat {A B : Type*} (R : Type*)
+  [semiring R] [add_comm_monoid A] [add_comm_monoid B] [module R B] :
+  (A →+ B) ≃ₗ[R] (A →ₗ[ℕ] B) :=
 { to_fun := add_monoid_hom.to_nat_linear_map,
   inv_fun := linear_map.to_add_monoid_hom,
   map_add' := by { intros, ext, refl },
@@ -648,11 +650,12 @@ def add_monoid_hom_lequiv_nat {A B : Type*} [add_comm_monoid A] [add_comm_monoid
   right_inv := by { intros f, ext, refl } }
 
 /--
-The `ℤ`-linear equivalence between additive morphisms `A →+ B` and `ℤ`-linear morphisms `A →ₗ[ℤ] B`.
+The `R`-linear equivalence between additive morphisms `A →+ B` and `ℤ`-linear morphisms `A →ₗ[ℤ] B`.
 -/
 @[simps]
-def add_monoid_hom_lequiv_int {A B : Type*} [add_comm_group A] [add_comm_group B] :
-  (A →+ B) ≃ₗ[ℤ] (A →ₗ[ℤ] B) :=
+def add_monoid_hom_lequiv_int {A B : Type*} (R : Type*)
+  [semiring R] [add_comm_group A] [add_comm_group B] [module R B] :
+  (A →+ B) ≃ₗ[R] (A →ₗ[ℤ] B) :=
 { to_fun := add_monoid_hom.to_int_linear_map,
   inv_fun := linear_map.to_add_monoid_hom,
   map_add' := by { intros, ext, refl },