chore(ring_theory/derivation): add leibniz_pow and leibniz_inv (#…

…9837)

src/ring_theory/derivation.lean

@@ -86,6 +86,17 @@ end
 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 leibniz_pow (n : ℕ) : D (a ^ n) = n • a ^ (n - 1) • D a :=
+begin
+  induction n with n ihn,
+  { rw [pow_zero, map_one_eq_zero, zero_smul] },
+  { rcases (zero_le n).eq_or_lt with (rfl|hpos),
+    { rw [pow_one, one_smul, pow_zero, one_smul] },
+    { have : a * a ^ (n - 1) = a ^ n, by rw [← pow_succ, nat.sub_add_cancel hpos],
+      simp only [pow_succ, leibniz, ihn, smul_comm a n, smul_smul a, add_smul, this,
+        nat.succ_eq_add_one, nat.add_succ_sub_one, add_zero, one_nsmul] } }
+end
+
 lemma eq_on_adjoin {s : set A} (h : set.eq_on D1 D2 s) : set.eq_on D1 D2 (adjoin R s) :=
 λ x hx, algebra.adjoin_induction hx h
   (λ r, (D1.map_algebra_map r).trans (D2.map_algebra_map r).symm)
@@ -198,6 +209,26 @@ variables (D : derivation R A M) {D1 D2 : derivation R A M} (r : R) (a b : A)
 @[simp] lemma map_neg : D (-a) = -D a := linear_map.map_neg D a
 @[simp] lemma map_sub : D (a - b) = D a - D b := linear_map.map_sub D a b
 
+lemma leibniz_of_mul_eq_one {a b : A} (h : a * b = 1) : D a = -a^2 • D b :=
+begin
+  rw neg_smul,
+  refine eq_neg_of_add_eq_zero _,
+  calc D a + a ^ 2 • D b = a • b • D a + a • a • D b : by simp only [smul_smul, h, one_smul, sq]
+                     ... = a • D (a * b)             : by rw [leibniz, smul_add, add_comm]
+                     ... = 0                         : by rw [h, map_one_eq_zero, smul_zero]
+end
+
+lemma leibniz_inv_of [invertible a] : D (⅟a) = -⅟a^2 • D a :=
+D.leibniz_of_mul_eq_one $ inv_of_mul_self a
+
+lemma leibniz_inv {K : Type*} [field K] [module K M] [algebra R K] [is_scalar_tower R K M]
+  (D : derivation R K M) (a : K) : D (a⁻¹) = -a⁻¹ ^ 2 • D a :=
+begin
+  rcases eq_or_ne a 0 with (rfl|ha),
+  { simp },
+  { exact D.leibniz_of_mul_eq_one (inv_mul_cancel ha) }
+end
+
 instance : has_neg (derivation R A M) :=
 ⟨λ D, { leibniz' := λ a b, by simp only [linear_map.neg_apply, smul_neg, neg_add_rev, leibniz,
           linear_map.to_fun_eq_coe, coe_fn_coe, add_comm],