feat(ring_theory/derivation): add 3 lemmas (#10996)

Add `map_smul_of_tower`, `map_coe_nat`, and `map_coe_int`.

Author: urkud

src/ring_theory/derivation.lean

@@ -86,12 +86,20 @@ protected lemma map_zero : D 0 = 0 := map_zero D
 @[simp] lemma map_smul : D (r • a) = r • D a := D.to_linear_map.map_smul r a
 @[simp] lemma leibniz : D (a * b) = a • D b + b • D a := D.leibniz' _ _
 
+@[simp, priority 900] lemma map_smul_of_tower {S : Type*} [has_scalar S A] [has_scalar S M]
+  [linear_map.compatible_smul A M S R] (D : derivation R A M) (r : S) (a : A) :
+  D (r • a) = r • D a :=
+D.to_linear_map.map_smul_of_tower r a
+
 @[simp] lemma map_one_eq_zero : D 1 = 0 := D.map_one_eq_zero'
 
 @[simp] lemma map_algebra_map : D (algebra_map R A r) = 0 :=
 by rw [←mul_one r, ring_hom.map_mul, ring_hom.map_one, ←smul_def, map_smul, map_one_eq_zero,
   smul_zero]
 
+@[simp] lemma map_coe_nat (n : ℕ) : D (n : A) = 0 :=
+by rw [← nsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]
+
 @[simp] lemma leibniz_pow (n : ℕ) : D (a ^ n) = n • a ^ (n - 1) • D a :=
 begin
   induction n with n ihn,
@@ -237,6 +245,9 @@ variables (D : derivation R A M) {D1 D2 : derivation R A M} (r : R) (a b : A)
 protected lemma map_neg : D (-a) = -D a := map_neg D a
 protected lemma map_sub : D (a - b) = D a - D b := map_sub D a b
 
+@[simp] lemma map_coe_int (n : ℤ) : D (n : A) = 0 :=
+by rw [← zsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]
+
 lemma leibniz_of_mul_eq_one {a b : A} (h : a * b = 1) : D a = -a^2 • D b :=
 begin
   rw neg_smul,