feat(ring_theory/power_series/basic): API about inv (#11617)

Also rename protected lemmas
`mul_inv`  to `mul_inv_cancel`
`inv_mul` to `inv_mul_cancel`

Author: pechersky

src/number_theory/bernoulli.lean

@@ -241,8 +241,8 @@ begin
   cases n, { simp },
   simp only [bernoulli_power_series, coeff_mul, coeff_X, sum_antidiagonal_succ', one_div, coeff_mk,
     coeff_one, coeff_exp, linear_map.map_sub, factorial, if_pos, cast_succ, cast_one, cast_mul,
-    sub_zero, ring_hom.map_one, add_eq_zero_iff, if_false, inv_one, zero_add, one_ne_zero, mul_zero,
-    and_false, sub_self, ← ring_hom.map_mul, ← ring_hom.map_sum],
+    sub_zero, ring_hom.map_one, add_eq_zero_iff, if_false, _root_.inv_one, zero_add, one_ne_zero,
+    mul_zero, and_false, sub_self, ← ring_hom.map_mul, ← ring_hom.map_sum],
   suffices : ∑ x in antidiagonal n, bernoulli x.1 / x.1! * ((x.2 + 1) * x.2!)⁻¹
            = if n.succ = 1 then 1 else 0, { split_ifs; simp [h, this] },
   cases n, { simp },

src/ring_theory/power_series/basic.lean

@@ -391,6 +391,10 @@ lemma coeff_smul (f : mv_power_series σ R) (n) (a : R) :
   coeff _ n (a • f) = a * coeff _ n f :=
 rfl
 
+lemma smul_eq_C_mul (f : mv_power_series σ R) (a : R) :
+  a • f = C σ R a * f :=
+by { ext, simp }
+
 lemma X_inj [nontrivial R] {s t : σ} : (X s : mv_power_series σ R) = X t ↔ s = t :=
 ⟨begin
   intro h, replace h := congr_arg (coeff R (single s 1)) h, rw [coeff_X, if_pos rfl, coeff_X] at h,
@@ -703,7 +707,10 @@ lemma inv_eq_zero {φ : mv_power_series σ k} :
   φ⁻¹ = 0 ↔ constant_coeff σ k φ = 0 :=
 ⟨λ h, by simpa using congr_arg (constant_coeff σ k) h,
  λ h, ext $ λ n, by { rw coeff_inv, split_ifs;
- simp only [h, mv_power_series.coeff_zero, zero_mul, inv_zero, neg_zero] }⟩
+  simp only [h, mv_power_series.coeff_zero, zero_mul, inv_zero, neg_zero] }⟩
+
+@[simp] lemma zero_inv : (0 : mv_power_series σ k)⁻¹ = 0 :=
+by rw [inv_eq_zero, constant_coeff_zero]
 
 @[simp, priority 1100]
 lemma inv_of_unit_eq (φ : mv_power_series σ k) (h : constant_coeff σ k φ ≠ 0) :
@@ -717,19 +724,19 @@ begin
   congr' 1, rw [units.ext_iff], exact h.symm,
 end
 
-@[simp] protected lemma mul_inv (φ : mv_power_series σ k) (h : constant_coeff σ k φ ≠ 0) :
+@[simp] protected lemma mul_inv_cancel (φ : mv_power_series σ k) (h : constant_coeff σ k φ ≠ 0) :
   φ * φ⁻¹ = 1 :=
 by rw [← inv_of_unit_eq φ h, mul_inv_of_unit φ (units.mk0 _ h) rfl]
 
-@[simp] protected lemma inv_mul (φ : mv_power_series σ k) (h : constant_coeff σ k φ ≠ 0) :
+@[simp] protected lemma inv_mul_cancel (φ : mv_power_series σ k) (h : constant_coeff σ k φ ≠ 0) :
   φ⁻¹ * φ = 1 :=
-by rw [mul_comm, φ.mul_inv h]
+by rw [mul_comm, φ.mul_inv_cancel h]
 
 protected lemma eq_mul_inv_iff_mul_eq {φ₁ φ₂ φ₃ : mv_power_series σ k}
   (h : constant_coeff σ k φ₃ ≠ 0) :
   φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂ :=
-⟨λ k, by simp [k, mul_assoc, mv_power_series.inv_mul _ h],
- λ k, by simp [← k, mul_assoc, mv_power_series.mul_inv _ h]⟩
+⟨λ k, by simp [k, mul_assoc, mv_power_series.inv_mul_cancel _ h],
+ λ k, by simp [← k, mul_assoc, mv_power_series.mul_inv_cancel _ h]⟩
 
 protected lemma eq_inv_iff_mul_eq_one {φ ψ : mv_power_series σ k} (h : constant_coeff σ k ψ ≠ 0) :
   φ = ψ⁻¹ ↔ φ * ψ = 1 :=
@@ -739,6 +746,39 @@ protected lemma inv_eq_iff_mul_eq_one {φ ψ : mv_power_series σ k} (h : consta
   ψ⁻¹ = φ ↔ φ * ψ = 1 :=
 by rw [eq_comm, mv_power_series.eq_inv_iff_mul_eq_one h]
 
+@[simp] protected lemma mul_inv_rev (φ ψ : mv_power_series σ k) :
+  (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹ :=
+begin
+  by_cases h : constant_coeff σ k (φ * ψ) = 0,
+  { rw inv_eq_zero.mpr h,
+    simp only [map_mul, mul_eq_zero] at h,
+    -- we don't have `no_zero_divisors (mw_power_series σ k)` yet,
+    cases h;
+    simp [inv_eq_zero.mpr h] },
+  { rw [mv_power_series.inv_eq_iff_mul_eq_one h],
+    simp only [not_or_distrib, map_mul, mul_eq_zero] at h,
+    rw [←mul_assoc, mul_assoc _⁻¹, mv_power_series.inv_mul_cancel _ h.left, mul_one,
+        mv_power_series.inv_mul_cancel _ h.right] }
+end
+
+@[simp] lemma one_inv : (1 : mv_power_series σ k)⁻¹ = 1 :=
+by { rw [mv_power_series.inv_eq_iff_mul_eq_one, mul_one], simp }
+
+@[simp] lemma C_inv (r : k) : (C σ k r)⁻¹ = C σ k r⁻¹ :=
+begin
+  rcases eq_or_ne r 0 with rfl|hr,
+  { simp },
+  rw [mv_power_series.inv_eq_iff_mul_eq_one, ←map_mul, inv_mul_cancel hr, map_one],
+  simpa using hr
+end
+
+@[simp] lemma X_inv (s : σ) : (X s : mv_power_series σ k)⁻¹ = 0 :=
+by rw [inv_eq_zero, constant_coeff_X]
+
+@[simp] lemma smul_inv (r : k) (φ : mv_power_series σ k) :
+  (r • φ)⁻¹ = r⁻¹ • φ⁻¹ :=
+by simp [smul_eq_C_mul, mul_comm]
+
 end field
 
 end mv_power_series
@@ -1050,6 +1090,10 @@ mv_power_series.coeff_C_mul _ φ a
   (n : ℕ) (φ : power_series S) (a : R) : coeff S n (a • φ) = a • coeff S n φ :=
 rfl
 
+lemma smul_eq_C_mul (f : power_series R) (a : R) :
+  a • f = C R a * f :=
+by { ext, simp }
+
 @[simp] lemma coeff_succ_mul_X (n : ℕ) (φ : power_series R) :
   coeff R (n+1) (φ * X) = coeff R n φ :=
 begin
@@ -1504,6 +1548,8 @@ lemma inv_eq_zero {φ : power_series k} :
   φ⁻¹ = 0 ↔ constant_coeff k φ = 0 :=
 mv_power_series.inv_eq_zero
 
+@[simp] lemma zero_inv : (0 : power_series k)⁻¹ = 0 := mv_power_series.zero_inv
+
 @[simp, priority 1100] lemma inv_of_unit_eq (φ : power_series k) (h : constant_coeff k φ ≠ 0) :
   inv_of_unit φ (units.mk0 _ h) = φ⁻¹ :=
 mv_power_series.inv_of_unit_eq _ _
@@ -1512,13 +1558,13 @@ mv_power_series.inv_of_unit_eq _ _
   inv_of_unit φ u = φ⁻¹ :=
 mv_power_series.inv_of_unit_eq' φ _ h
 
-@[simp] protected lemma mul_inv (φ : power_series k) (h : constant_coeff k φ ≠ 0) :
+@[simp] protected lemma mul_inv_cancel (φ : power_series k) (h : constant_coeff k φ ≠ 0) :
   φ * φ⁻¹ = 1 :=
-mv_power_series.mul_inv φ h
+mv_power_series.mul_inv_cancel φ h
 
-@[simp] protected lemma inv_mul (φ : power_series k) (h : constant_coeff k φ ≠ 0) :
+@[simp] protected lemma inv_mul_cancel (φ : power_series k) (h : constant_coeff k φ ≠ 0) :
   φ⁻¹ * φ = 1 :=
-mv_power_series.inv_mul φ h
+mv_power_series.inv_mul_cancel φ h
 
 lemma eq_mul_inv_iff_mul_eq {φ₁ φ₂ φ₃ : power_series k} (h : constant_coeff k φ₃ ≠ 0) :
   φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂ :=
@@ -1532,6 +1578,23 @@ lemma inv_eq_iff_mul_eq_one {φ ψ : power_series k} (h : constant_coeff k ψ 
   ψ⁻¹ = φ ↔ φ * ψ = 1 :=
 mv_power_series.inv_eq_iff_mul_eq_one h
 
+@[simp] protected lemma mul_inv_rev (φ ψ : power_series k) :
+  (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹ :=
+mv_power_series.mul_inv_rev _ _
+
+@[simp] lemma one_inv : (1 : power_series k)⁻¹ = 1 :=
+mv_power_series.one_inv
+
+@[simp] lemma C_inv (r : k) : (C k r)⁻¹ = C k r⁻¹ :=
+mv_power_series.C_inv _
+
+@[simp] lemma X_inv : (X : power_series k)⁻¹ = 0 :=
+mv_power_series.X_inv _
+
+@[simp] lemma smul_inv (r : k) (φ : power_series k) :
+  (r • φ)⁻¹ = r⁻¹ • φ⁻¹ :=
+mv_power_series.smul_inv _ _
+
 end field
 
 end power_series
@@ -1836,6 +1899,8 @@ by rw [bit1, bit1, coe_add, coe_one, coe_bit0]
   ((X : polynomial R) : power_series R) = power_series.X :=
 coe_monomial _ _
 
+@[simp] lemma constant_coeff_coe : power_series.constant_coeff R φ = φ.coeff 0 := rfl
+
 variables (R)
 
 lemma coe_injective : function.injective (coe : polynomial R → power_series R) :=