feat(*): generalize to and add distrib_smul instances (#16132)

This PR builds on #16123 by adding `distrib_smul` (and `smul_zero_class`) instances for:
 * `finsupp`
 * `add_monoid_algebra`
 * `polynomial`
 * submodule quotients
 * scalar multiplication by `ℚ`

It also generalizes some results by weakening `distrib_mul_action` to `distrib_smul`. The choice of instances and generalizations is based on which are necessary to solve instance diamonds in `splitting_field`, so I probably missed a lot of additional changes. Since I'm not so interested in generalizing everything at the moment, I'd rather leave missing instances to follow-up PRs.



Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>

src/algebra/monoid_algebra/basic.lean

@@ -268,9 +268,13 @@ instance [comm_ring k] [comm_monoid G] : comm_ring (monoid_algebra k G) :=
 
 variables {S : Type*}
 
-instance [monoid R] [semiring k] [distrib_mul_action R k] :
-  has_smul R (monoid_algebra k G) :=
-finsupp.has_smul
+instance [semiring k] [smul_zero_class R k] :
+  smul_zero_class R (monoid_algebra k G) :=
+finsupp.smul_zero_class
+
+instance [semiring k] [distrib_smul R k] :
+  distrib_smul R (monoid_algebra k G) :=
+finsupp.distrib_smul _ _
 
 instance [monoid R] [semiring k] [distrib_mul_action R k] :
   distrib_mul_action R (monoid_algebra k G) :=
@@ -451,7 +455,7 @@ end misc_theorems
 /-! #### Non-unital, non-associative algebra structure -/
 section non_unital_non_assoc_algebra
 
-variables (k) [monoid R] [semiring k] [distrib_mul_action R k] [has_mul G]
+variables (k) [semiring k] [distrib_smul R k] [has_mul G]
 
 instance is_scalar_tower_self [is_scalar_tower R k k] :
   is_scalar_tower R (monoid_algebra k G) (monoid_algebra k G) :=
@@ -999,9 +1003,9 @@ end mul_one_class
 /-! #### Semiring structure -/
 section semiring
 
-instance {R : Type*} [monoid R] [semiring k] [distrib_mul_action R k] :
-  has_smul R (add_monoid_algebra k G) :=
-finsupp.has_smul
+instance {R : Type*} [semiring k] [smul_zero_class R k] :
+  smul_zero_class R (add_monoid_algebra k G) :=
+finsupp.smul_zero_class
 
 variables [semiring k] [add_monoid G]
 
@@ -1298,22 +1302,22 @@ variables {k G}
 
 section non_unital_non_assoc_algebra
 
-variables (k) [monoid R] [semiring k] [distrib_mul_action R k] [has_add G]
+variables (k) [semiring k] [distrib_smul R k] [has_add G]
 
 instance is_scalar_tower_self [is_scalar_tower R k k] :
   is_scalar_tower R (add_monoid_algebra k G) (add_monoid_algebra k G) :=
-@monoid_algebra.is_scalar_tower_self k (multiplicative G) R _ _ _ _ _
+@monoid_algebra.is_scalar_tower_self k (multiplicative G) R _ _ _ _
 
 /-- Note that if `k` is a `comm_semiring` then we have `smul_comm_class k k k` and so we can take
 `R = k` in the below. In other words, if the coefficients are commutative amongst themselves, they
 also commute with the algebra multiplication. -/
 instance smul_comm_class_self [smul_comm_class R k k] :
   smul_comm_class R (add_monoid_algebra k G) (add_monoid_algebra k G) :=
-@monoid_algebra.smul_comm_class_self k (multiplicative G) R _ _ _ _ _
+@monoid_algebra.smul_comm_class_self k (multiplicative G) R _ _ _ _
 
 instance smul_comm_class_symm_self [smul_comm_class k R k] :
   smul_comm_class (add_monoid_algebra k G) R (add_monoid_algebra k G) :=
-@monoid_algebra.smul_comm_class_symm_self k (multiplicative G) R _ _ _ _ _
+@monoid_algebra.smul_comm_class_symm_self k (multiplicative G) R _ _ _ _
 
 variables {A : Type u₃} [non_unital_non_assoc_semiring A]
 

src/data/finsupp/basic.lean

@@ -1296,36 +1296,42 @@ end
 end
 
 section
-instance [monoid R] [add_monoid M] [distrib_mul_action R M] : has_smul R (α →₀ M) :=
-⟨λa v, v.map_range ((•) a) (smul_zero _)⟩
+
+instance [has_zero M] [smul_zero_class R M] : smul_zero_class R (α →₀ M) :=
+{ smul := λ a v, v.map_range ((•) a) (smul_zero _),
+  smul_zero := λ a, by { ext, apply smul_zero } }
 
 /-!
 Throughout this section, some `monoid` and `semiring` arguments are specified with `{}` instead of
 `[]`. See note [implicit instance arguments].
 -/
 
-@[simp] lemma coe_smul {_ : monoid R} [add_monoid M] [distrib_mul_action R M]
+@[simp] lemma coe_smul [add_monoid M] [distrib_smul R M]
   (b : R) (v : α →₀ M) : ⇑(b • v) = b • v := rfl
-lemma smul_apply {_ : monoid R} [add_monoid M] [distrib_mul_action R M]
+lemma smul_apply [add_monoid M] [distrib_smul R M]
   (b : R) (v : α →₀ M) (a : α) : (b • v) a = b • (v a) := rfl
 
-lemma _root_.is_smul_regular.finsupp {_ : monoid R} [add_monoid M] [distrib_mul_action R M] {k : R}
+lemma _root_.is_smul_regular.finsupp [add_monoid M] [distrib_smul R M] {k : R}
   (hk : is_smul_regular M k) : is_smul_regular (α →₀ M) k :=
 λ _ _ h, ext $ λ i, hk (congr_fun h i)
 
-instance [monoid R] [nonempty α] [add_monoid M] [distrib_mul_action R M] [has_faithful_smul R M] :
+instance [nonempty α] [add_monoid M] [distrib_smul R M] [has_faithful_smul R M] :
   has_faithful_smul R (α →₀ M) :=
 { eq_of_smul_eq_smul := λ r₁ r₂ h, let ⟨a⟩ := ‹nonempty α› in eq_of_smul_eq_smul $ λ m : M,
     by simpa using congr_fun (h (single a m)) a }
 
 variables (α M)
 
-instance [monoid R] [add_monoid M] [distrib_mul_action R M] : distrib_mul_action R (α →₀ M) :=
+instance [add_zero_class M] [distrib_smul R M] : distrib_smul R (α →₀ M) :=
 { smul      := (•),
   smul_add  := λ a x y, ext $ λ _, smul_add _ _ _,
+  smul_zero := λ x, ext $ λ _, smul_zero _ }
+
+instance [monoid R] [add_monoid M] [distrib_mul_action R M] : distrib_mul_action R (α →₀ M) :=
+{ smul      := (•),
   one_smul  := λ x, ext $ λ _, one_smul _ _,
   mul_smul  := λ r s x, ext $ λ _, mul_smul _ _ _,
-  smul_zero := λ x, ext $ λ _, smul_zero _ }
+  ..finsupp.distrib_smul _ _ }
 
 instance [monoid R] [monoid S] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action S M]
   [has_smul R S] [is_scalar_tower R S M] :
@@ -1416,14 +1422,14 @@ lemma sum_smul_index [semiring R] [add_comm_monoid M] {g : α →₀ R} {b : R}
   (h0 : ∀i, h i 0 = 0) : (b • g).sum h = g.sum (λi a, h i (b * a)) :=
 finsupp.sum_map_range_index h0
 
-lemma sum_smul_index' [monoid R] [add_monoid M] [distrib_mul_action R M] [add_comm_monoid N]
+lemma sum_smul_index' [add_monoid M] [distrib_smul R M] [add_comm_monoid N]
   {g : α →₀ M} {b : R} {h : α → M → N} (h0 : ∀i, h i 0 = 0) :
   (b • g).sum h = g.sum (λi c, h i (b • c)) :=
 finsupp.sum_map_range_index h0
 
 /-- A version of `finsupp.sum_smul_index'` for bundled additive maps. -/
 lemma sum_smul_index_add_monoid_hom
-  [monoid R] [add_monoid M] [add_comm_monoid N] [distrib_mul_action R M]
+  [add_monoid M] [add_comm_monoid N] [distrib_smul R M]
   {g : α →₀ M} {b : R} {h : α → M →+ N} :
   (b • g).sum (λ a, h a) = g.sum (λ i c, h i (b • c)) :=
 sum_map_range_index (λ i, (h i).map_zero)

src/data/polynomial/basic.lean

@@ -97,8 +97,9 @@ instance : has_add R[X] := ⟨add⟩
 instance {R : Type u} [ring R] : has_neg R[X] := ⟨neg⟩
 instance {R : Type u} [ring R] : has_sub R[X] := ⟨λ a b, a + -b⟩
 instance : has_mul R[X] := ⟨mul⟩
-instance {S : Type*} [monoid S] [distrib_mul_action S R] : has_smul S R[X] :=
-⟨λ r p, ⟨r • p.to_finsupp⟩⟩
+instance {S : Type*} [smul_zero_class S R] : smul_zero_class S R[X] :=
+{ smul := λ r p, ⟨r • p.to_finsupp⟩,
+  smul_zero := λ a, congr_arg of_finsupp (smul_zero a) }
 @[priority 1]  -- to avoid a bug in the `ring` tactic
 instance has_pow : has_pow R[X] ℕ := { pow := λ p n, npow_rec n p }
 
@@ -111,7 +112,7 @@ show _ = neg _, by rw neg
 @[simp] lemma of_finsupp_sub {R : Type u} [ring R] {a b} : (⟨a - b⟩ : R[X]) = ⟨a⟩ - ⟨b⟩ :=
 by { rw [sub_eq_add_neg, of_finsupp_add, of_finsupp_neg], refl }
 @[simp] lemma of_finsupp_mul (a b) : (⟨a * b⟩ : R[X]) = ⟨a⟩ * ⟨b⟩ := show _ = mul _ _, by rw mul
-@[simp] lemma of_finsupp_smul {S : Type*} [monoid S] [distrib_mul_action S R] (a : S) (b) :
+@[simp] lemma of_finsupp_smul {S : Type*} [smul_zero_class S R] (a : S) (b) :
   (⟨a • b⟩ : R[X]) = (a • ⟨b⟩ : R[X]) := rfl
 @[simp] lemma of_finsupp_pow (a) (n : ℕ) : (⟨a ^ n⟩ : R[X]) = ⟨a⟩ ^ n :=
 begin
@@ -136,7 +137,7 @@ by { cases a, rw ←of_finsupp_neg }
 by { rw [sub_eq_add_neg, ←to_finsupp_neg, ←to_finsupp_add], refl }
 @[simp] lemma to_finsupp_mul (a b : R[X]) : (a * b).to_finsupp = a.to_finsupp * b.to_finsupp :=
 by { cases a, cases b, rw ←of_finsupp_mul }
-@[simp] lemma to_finsupp_smul {S : Type*} [monoid S] [distrib_mul_action S R] (a : S) (b : R[X]) :
+@[simp] lemma to_finsupp_smul {S : Type*} [smul_zero_class S R] (a : S) (b : R[X]) :
   (a • b).to_finsupp = a • b.to_finsupp := rfl
 @[simp] lemma to_finsupp_pow (a : R[X]) (n : ℕ) : (a ^ n).to_finsupp = a.to_finsupp ^ n :=
 by { cases a, rw ←of_finsupp_pow }
@@ -196,6 +197,11 @@ instance {S₁ S₂} [has_smul S₁ S₂] [monoid S₁] [monoid S₂] [distrib_m
   [distrib_mul_action S₂ R] [is_scalar_tower S₁ S₂ R] : is_scalar_tower S₁ S₂ R[X] :=
 ⟨by { rintros _ _ ⟨⟩, simp_rw [←of_finsupp_smul, smul_assoc] }⟩
 
+instance is_scalar_tower_right {α K : Type*} [semiring K] [distrib_smul α K]
+  [is_scalar_tower α K K] : is_scalar_tower α K[X] K[X] :=
+⟨by rintros _ ⟨⟩ ⟨⟩;
+  simp_rw [smul_eq_mul, ← of_finsupp_smul, ← of_finsupp_mul, ← of_finsupp_smul, smul_mul_assoc]⟩
+
 instance {S} [monoid S] [distrib_mul_action S R] [distrib_mul_action Sᵐᵒᵖ R]
   [is_central_scalar S R] : is_central_scalar S R[X] :=
 ⟨by { rintros _ ⟨⟩, simp_rw [←of_finsupp_smul, op_smul_eq_smul] }⟩

src/data/rat/cast.lean

@@ -350,3 +350,22 @@ by rw [cast_def, div_eq_mul_inv, unop_mul, unop_inv, unop_nat_cast, unop_int_cas
     (commute.cast_int_right _ r.num).eq, cast_def, div_eq_mul_inv]
 
 end mul_opposite
+
+section smul
+
+namespace rat
+
+variables {K : Type*} [division_ring K]
+
+@[priority 100]
+instance distrib_smul  : distrib_smul ℚ K :=
+{ smul := (•),
+  smul_zero := λ a, by rw [smul_def, mul_zero],
+  smul_add := λ a x y, by simp only [smul_def, mul_add, cast_add] }
+
+instance is_scalar_tower_right : is_scalar_tower ℚ K K :=
+⟨λ a x y, by simp only [smul_def, smul_eq_mul, mul_assoc]⟩
+
+end rat
+
+end smul

src/field_theory/ratfunc.lean

@@ -140,15 +140,17 @@ of `∀ {p q a : K[X]} (hq : q ≠ 0) (ha : a ≠ 0), f (a * p) (a * q) = f p q)
   (H : ∀ {p q p' q'} (hq : q ∈ K[X]⁰) (hq' : q' ∈ K[X]⁰), p * q' = p' * q →
     f p q = f p' q') :
   P :=
-localization.lift_on (to_fraction_ring x) (λ p q, f p q) (λ p p' q q' h, H q.2 q'.2
+localization.lift_on
+  (by exact to_fraction_ring x) -- Fix timeout by manipulating elaboration order
+  (λ p q, f p q) (λ p p' q q' h, H q.2 q'.2
   (let ⟨⟨c, hc⟩, mul_eq⟩ := (localization.r_iff_exists).mp h in
     mul_cancel_right_coe_non_zero_divisor.mp mul_eq))
 
 lemma lift_on_of_fraction_ring_mk {P : Sort v} (n : K[X]) (d : K[X]⁰)
   (f : ∀ (p q : K[X]), P)
   (H : ∀ {p q p' q'} (hq : q ∈ K[X]⁰) (hq' : q' ∈ K[X]⁰), p * q' = p' * q →
     f p q = f p' q') :
-  ratfunc.lift_on (of_fraction_ring (localization.mk n d)) f @H = f n d :=
+  ratfunc.lift_on (by exact of_fraction_ring (localization.mk n d)) f @H = f n d :=
 begin
   unfold ratfunc.lift_on,
   exact localization.lift_on_mk _ _ _ _

src/group_theory/group_action/big_operators.lean

@@ -19,11 +19,11 @@ variables {α β γ : Type*}
 open_locale big_operators
 
 section
-variables [monoid α] [add_monoid β] [distrib_mul_action α β]
+variables [add_monoid β] [distrib_smul α β]
 
 lemma list.smul_sum {r : α} {l : list β} :
   r • l.sum = (l.map ((•) r)).sum :=
-(distrib_mul_action.to_add_monoid_hom β r).map_list_sum l
+(distrib_smul.to_add_monoid_hom β r).map_list_sum l
 
 end
 
@@ -37,15 +37,15 @@ lemma list.smul_prod {r : α} {l : list β} :
 end
 
 section
-variables [monoid α] [add_comm_monoid β] [distrib_mul_action α β]
+variables [add_comm_monoid β] [distrib_smul α β]
 
 lemma multiset.smul_sum {r : α} {s : multiset β} :
   r • s.sum = (s.map ((•) r)).sum :=
-(distrib_mul_action.to_add_monoid_hom β r).map_multiset_sum s
+(distrib_smul.to_add_monoid_hom β r).map_multiset_sum s
 
 lemma finset.smul_sum {r : α} {f : γ → β} {s : finset γ} :
   r • ∑ x in s, f x = ∑ x in s, r • f x :=
-(distrib_mul_action.to_add_monoid_hom β r).map_sum f s
+(distrib_smul.to_add_monoid_hom β r).map_sum f s
 
 end