feat(algebra & polynomial): some (q)smul lemmas+generalisations (#18852)

There is many generalisations around these areas too, but I am specifically not doing them as it will be easier done after the port. I am only doing what I need for merging in the splitting field diamond fix.



Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

src/algebra/algebra/basic.lean

@@ -606,12 +606,6 @@ by rw [←algebra.commutes, ←algebra.commutes, map_algebra_map_mul]
 
 end linear_map
 
-
-@[simp] lemma rat.smul_one_eq_coe {A : Type*} [division_ring A] [algebra ℚ A] (m : ℚ) :
-  @@has_smul.smul algebra.to_has_smul m (1 : A) = ↑m :=
-by rw [algebra.smul_def, mul_one, eq_rat_cast]
-
-
 section nat
 
 variables {R : Type*} [semiring R]

src/algebra/field/defs.lean

@@ -143,6 +143,10 @@ instance smul_division_ring : has_smul ℚ K :=
 
 lemma smul_def (a : ℚ) (x : K) : a • x = ↑a * x := division_ring.qsmul_eq_mul' a x
 
+@[simp] lemma smul_one_eq_coe (A : Type*) [division_ring A] (m : ℚ) :
+  m • (1 : A) = ↑m :=
+by rw [rat.smul_def, mul_one]
+
 end rat
 
 end division_ring

src/algebra/monoid_algebra/basic.lean

@@ -1123,6 +1123,9 @@ instance [comm_ring k] [add_comm_monoid G] : comm_ring (add_monoid_algebra k G)
 
 variables {S : Type*}
 
+instance [semiring k] [distrib_smul R k] : distrib_smul R (add_monoid_algebra k G) :=
+finsupp.distrib_smul G k
+
 instance [monoid R] [semiring k] [distrib_mul_action R k] :
   distrib_mul_action R (add_monoid_algebra k G) :=
 finsupp.distrib_mul_action G k

src/data/finsupp/basic.lean

@@ -1259,16 +1259,16 @@ Throughout this section, some `monoid` and `semiring` arguments are specified wi
 `[]`. See note [implicit instance arguments].
 -/
 
-@[simp] lemma coe_smul [add_monoid M] [distrib_smul R M]
+@[simp] lemma coe_smul [add_monoid M] [smul_zero_class R M]
   (b : R) (v : α →₀ M) : ⇑(b • v) = b • v := rfl
-lemma smul_apply [add_monoid M] [distrib_smul R M]
+lemma smul_apply [add_monoid M] [smul_zero_class R M]
   (b : R) (v : α →₀ M) (a : α) : (b • v) a = b • (v a) := rfl
 
-lemma _root_.is_smul_regular.finsupp [add_monoid M] [distrib_smul R M] {k : R}
+lemma _root_.is_smul_regular.finsupp [add_monoid M] [smul_zero_class R M] {k : R}
   (hk : is_smul_regular M k) : is_smul_regular (α →₀ M) k :=
 λ _ _ h, ext $ λ i, hk (congr_fun h i)
 
-instance [nonempty α] [add_monoid M] [distrib_smul R M] [has_faithful_smul R M] :
+instance [nonempty α] [add_monoid M] [smul_zero_class 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 }
@@ -1286,18 +1286,16 @@ instance [monoid R] [add_monoid M] [distrib_mul_action R M] : distrib_mul_action
   mul_smul  := λ r s x, ext $ λ _, mul_smul _ _ _,
   ..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] :
-  is_scalar_tower R S (α →₀ M) :=
+instance [has_zero M] [smul_zero_class R M] [smul_zero_class S M] [has_smul R S]
+  [is_scalar_tower R S M] : is_scalar_tower R S (α →₀ M) :=
 { smul_assoc := λ r s a, ext $ λ _, smul_assoc _ _ _ }
 
-instance [monoid R] [monoid S] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action S M]
-  [smul_comm_class R S M] :
-  smul_comm_class R S (α →₀ M) :=
+instance [has_zero M] [smul_zero_class R M] [smul_zero_class S M]
+  [smul_comm_class R S M] : smul_comm_class R S (α →₀ M) :=
 { smul_comm := λ r s a, ext $ λ _, smul_comm _ _ _ }
 
-instance [monoid R] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M]
-  [is_central_scalar R M] : is_central_scalar R (α →₀ M) :=
+instance [has_zero M] [smul_zero_class R M] [smul_zero_class Rᵐᵒᵖ M] [is_central_scalar R M] :
+  is_central_scalar R (α →₀ M) :=
 { op_smul_eq_smul := λ r a, ext $ λ _, op_smul_eq_smul _ _ }
 
 instance [semiring R] [add_comm_monoid M] [module R M] : module R (α →₀ M) :=
@@ -1332,7 +1330,7 @@ lemma map_domain_smul {_ : monoid R} [add_comm_monoid M] [distrib_mul_action R M
    {f : α → β} (b : R) (v : α →₀ M) : map_domain f (b • v) = b • map_domain f v :=
 map_domain_map_range _ _ _ _ (smul_add b)
 
-@[simp] lemma smul_single {_ : monoid R} [add_monoid M] [distrib_mul_action R M]
+@[simp] lemma smul_single [has_zero M] [smul_zero_class R M]
   (c : R) (a : α) (b : M) : c • finsupp.single a b = finsupp.single a (c • b) :=
 map_range_single
 

src/data/polynomial/basic.lean

@@ -183,6 +183,10 @@ function.injective.semiring to_finsupp to_finsupp_injective
   to_finsupp_zero to_finsupp_one to_finsupp_add to_finsupp_mul
   (λ _ _, to_finsupp_smul _ _) to_finsupp_pow (λ _, rfl)
 
+instance {S} [distrib_smul S R] : distrib_smul S R[X] :=
+function.injective.distrib_smul ⟨to_finsupp, to_finsupp_zero, to_finsupp_add⟩
+to_finsupp_injective to_finsupp_smul
+
 instance {S} [monoid S] [distrib_mul_action S R] : distrib_mul_action S R[X] :=
 function.injective.distrib_mul_action
   ⟨to_finsupp, to_finsupp_zero, to_finsupp_add⟩ to_finsupp_injective to_finsupp_smul
@@ -301,7 +305,7 @@ begin
   { simp [pow_succ, ih, monomial_mul_monomial, nat.succ_eq_add_one, mul_add, add_comm] },
 end
 
-lemma smul_monomial {S} [monoid S] [distrib_mul_action S R] (a : S) (n : ℕ) (b : R) :
+lemma smul_monomial {S} [smul_zero_class S R] (a : S) (n : ℕ) (b : R) :
   a • monomial n b = monomial n (a • b) :=
 to_finsupp_injective $ by simp
 
@@ -342,7 +346,7 @@ lemma C_mul : C (a * b) = C a * C b := C.map_mul a b
 
 lemma C_add : C (a + b) = C a + C b := C.map_add a b
 
-@[simp] lemma smul_C {S} [monoid S] [distrib_mul_action S R] (s : S) (r : R) :
+@[simp] lemma smul_C {S} [smul_zero_class S R] (s : S) (r : R) :
   s • C r = C (s • r) :=
 smul_monomial _ _ r
 
@@ -857,6 +861,15 @@ mt (congr_arg (λ p, coeff p 1)) (by simp)
 
 end nonzero_semiring
 
+section division_ring
+
+variables [division_ring R]
+
+lemma rat_smul_eq_C_mul (a : ℚ) (f : R[X]) : a • f = polynomial.C ↑a * f :=
+by rw [←rat.smul_one_eq_coe, ←polynomial.smul_C, C_1, smul_one_mul]
+
+end division_ring
+
 @[simp] lemma nontrivial_iff [semiring R] : nontrivial R[X] ↔ nontrivial R :=
 ⟨λ h, let ⟨r, s, hrs⟩ := @exists_pair_ne _ h in nontrivial.of_polynomial_ne hrs,
   λ h, @polynomial.nontrivial _ _ h⟩

src/data/polynomial/coeff.lean

@@ -41,7 +41,7 @@ by { rcases p, rcases q, simp_rw [←of_finsupp_add, coeff], exact finsupp.add_a
 
 @[simp] lemma coeff_bit0 (p : R[X]) (n : ℕ) : coeff (bit0 p) n = bit0 (coeff p n) := by simp [bit0]
 
-@[simp] lemma coeff_smul [monoid S] [distrib_mul_action S R] (r : S) (p : R[X]) (n : ℕ) :
+@[simp] lemma coeff_smul [smul_zero_class S R] (r : S) (p : R[X]) (n : ℕ) :
   coeff (r • p) n = r • coeff p n :=
 by { rcases p, simp_rw [←of_finsupp_smul, coeff], exact finsupp.smul_apply _ _ _ }