[Merged by Bors] - feat(data/dfinsupp): Relax requirements of semimodule conversion to add_comm_monoid

src/algebra/direct_limit.lean

@@ -172,7 +172,7 @@ span_induction ((quotient.mk_eq_zero _).1 H)
           to_module_totalize_of_le hik hi,
           to_module_totalize_of_le hjk hj]⟩)
   (λ a x ⟨i, hi, hxi⟩,
-    ⟨i, λ k hk, hi k (dfinsupp.support_smul hk),
+    ⟨i, λ k hk, hi k (@dfinsupp.support_smul ι G _ _ _ _ _ _ _ _ _ hk),
       by simp [linear_map.map_smul, hxi]⟩)
 
 /-- A component that corresponds to zero in the direct limit is already zero in some

src/algebra/lie/basic.lean

@@ -314,7 +314,7 @@ instance : lie_ring (⨁ i, L i) :=
 
 /-- The direct sum of Lie algebras carries a natural Lie algebra structure. -/
 instance : lie_algebra R (⨁ i, L i) :=
-{ lie_smul := λ c x y, by { ext, simp only [zip_with_apply, smul_apply, bracket_apply, lie_smul], },
+{ lie_smul := λ c x y, by { ext, simp only [zip_with_apply, @smul_apply ι L _ _ _ _ _ _ _, bracket_apply, lie_smul],},
   ..(infer_instance : module R _) }
 
 end direct_sum

src/data/dfinsupp.lean

@@ -146,21 +146,22 @@ instance [Π i, add_comm_group (β i)] : add_comm_group (Π₀ i, β i) :=
 
 /-- Dependent functions with finite support inherit a semiring action from an action on each
 coordinate. -/
-def to_has_scalar {γ : Type w} [semiring γ] [Π i, add_comm_group (β i)] [Π i, semimodule γ (β i)] :
+def to_has_scalar {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)] :
   has_scalar γ (Π₀ i, β i) :=
 ⟨λc v, v.map_range (λ _, (•) c) (λ _, smul_zero _)⟩
 local attribute [instance] to_has_scalar
 
-@[simp] lemma smul_apply {γ : Type w} [semiring γ] [Π i, add_comm_group (β i)]
+@[simp] lemma smul_apply {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)]
   [Π i, semimodule γ (β i)] {i : ι} {b : γ} {v : Π₀ i, β i} :
   (b • v) i = b • (v i) :=
 map_range_apply
 
 /-- Dependent functions with finite support inherit a semimodule structure from such a structure on
 each coordinate. -/
-def to_semimodule {γ : Type w} [semiring γ] [Π i, add_comm_group (β i)] [Π i, semimodule γ (β i)] :
-  semimodule γ (Π₀ i, β i) :=
-semimodule.of_core {
+def to_semimodule {γ : Type w} [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)] :
+  semimodule γ (Π₀ i, β i) := {
+  smul_zero := λ c, ext $ λ i, by simp only [smul_apply, smul_zero, zero_apply],
+  zero_smul := λ c, ext $ λ i, by simp only [smul_apply, zero_smul, zero_apply],
   smul_add := λ c x y, ext $ λ i, by simp only [add_apply, smul_apply, smul_add],
   add_smul := λ c x y, ext $ λ i, by simp only [add_apply, smul_apply, add_smul],
   one_smul := λ x, ext $ λ i, by simp only [smul_apply, one_smul],
@@ -427,7 +428,7 @@ instance [Π i, add_group (β i)] {s : finset ι} : is_add_group_hom (@mk ι β
 
 section
 local attribute [instance] to_semimodule
-variables (γ : Type w) [semiring γ] [Π i, add_comm_group (β i)] [Π i, semimodule γ (β i)]
+variables (γ : Type w) [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)]
 include γ
 
 @[simp] lemma mk_smul {s : finset ι} {c : γ} (x : Π i : (↑s : set ι), β i.1) :
@@ -604,7 +605,7 @@ by ext i; simp
 
 local attribute [instance] dfinsupp.to_semimodule
 
-lemma support_smul {γ : Type w} [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)]
+lemma support_smul {γ : Type w} [ring γ] [Π i, add_comm_monoid (β i)] [Π i, semimodule γ (β i)]
   [Π (i : ι) (x : β i), decidable (x ≠ 0)]
   {b : γ} {v : Π₀ i, β i} : (b • v).support ⊆ v.support :=
 support_map_range

src/linear_algebra/direct_sum_module.lean

@@ -36,7 +36,7 @@ open_locale direct_sum
 
 variables {R ι M}
 
-instance : semimodule R (⨁ i, M i) := dfinsupp.to_semimodule
+instance : semimodule R (⨁ i, M i) := @dfinsupp.to_semimodule ι M _ _ _ _
 
 include dec_ι