chore(algebra/group_with_zero/basic): move ring.inverse, generalize…

… and rename `inverse_eq_has_inv` (#10033)

This moves `ring.inverse` earlier in the import graph, since it's not about rings at all.

src/algebra/field.lean

@@ -65,14 +65,6 @@ instance division_ring.to_group_with_zero :
 { .. ‹division_ring K›,
   .. (infer_instance : semiring K) }
 
-lemma inverse_eq_has_inv : (ring.inverse : K → K) = has_inv.inv :=
-begin
-  ext x,
-  by_cases hx : x = 0,
-  { simp [hx] },
-  { exact ring.inverse_unit (units.mk0 x hx) }
-end
-
 attribute [field_simps] inv_eq_one_div
 
 local attribute [simp]

src/algebra/group_with_zero/basic.lean

@@ -339,6 +339,60 @@ end is_unit
 @[simp] theorem not_is_unit_zero [nontrivial M₀] : ¬ is_unit (0 : M₀) :=
 mt is_unit_zero_iff.1 zero_ne_one
 
+namespace ring
+open_locale classical
+
+/-- Introduce a function `inverse` on a monoid with zero `M₀`, which sends `x` to `x⁻¹` if `x` is
+invertible and to `0` otherwise.  This definition is somewhat ad hoc, but one needs a fully (rather
+than partially) defined inverse function for some purposes, including for calculus.
+
+Note that while this is in the `ring` namespace for brevity, it requires the weaker assumption
+`monoid_with_zero M₀` instead of `ring M₀`. -/
+noncomputable def inverse : M₀ → M₀ :=
+λ x, if h : is_unit x then ((h.unit⁻¹ : units M₀) : M₀) else 0
+
+/-- By definition, if `x` is invertible then `inverse x = x⁻¹`. -/
+@[simp] lemma inverse_unit (u : units M₀) : inverse (u : M₀) = (u⁻¹ : units M₀) :=
+begin
+  simp only [units.is_unit, inverse, dif_pos],
+  exact units.inv_unique rfl
+end
+
+/-- By definition, if `x` is not invertible then `inverse x = 0`. -/
+@[simp] lemma inverse_non_unit (x : M₀) (h : ¬(is_unit x)) : inverse x = 0 := dif_neg h
+
+lemma mul_inverse_cancel (x : M₀) (h : is_unit x) : x * inverse x = 1 :=
+by { rcases h with ⟨u, rfl⟩, rw [inverse_unit, units.mul_inv], }
+
+lemma inverse_mul_cancel (x : M₀) (h : is_unit x) : inverse x * x = 1 :=
+by { rcases h with ⟨u, rfl⟩, rw [inverse_unit, units.inv_mul], }
+
+lemma mul_inverse_cancel_right (x y : M₀) (h : is_unit x) : y * x * inverse x = y :=
+by rw [mul_assoc, mul_inverse_cancel x h, mul_one]
+
+lemma inverse_mul_cancel_right (x y : M₀) (h : is_unit x) : y * inverse x * x = y :=
+by rw [mul_assoc, inverse_mul_cancel x h, mul_one]
+
+lemma mul_inverse_cancel_left (x y : M₀) (h : is_unit x) : x * (inverse x * y) = y :=
+by rw [← mul_assoc, mul_inverse_cancel x h, one_mul]
+
+lemma inverse_mul_cancel_left (x y : M₀) (h : is_unit x) : inverse x * (x * y) = y :=
+by rw [← mul_assoc, inverse_mul_cancel x h, one_mul]
+
+lemma mul_inverse_rev {M₀ : Type*} [comm_monoid_with_zero M₀] (a b : M₀) :
+  ring.inverse (a * b) = ring.inverse b * ring.inverse a :=
+begin
+  by_cases hab : is_unit (a * b),
+  { obtain ⟨⟨a, rfl⟩, b, rfl⟩ := is_unit.mul_iff.mp hab,
+    rw [←units.coe_mul, ring.inverse_unit, ring.inverse_unit, ring.inverse_unit, ←units.coe_mul,
+      mul_inv_rev], },
+  obtain ha | hb := not_and_distrib.mp (mt is_unit.mul_iff.mpr hab),
+  { rw [ring.inverse_non_unit _ hab, ring.inverse_non_unit _ ha, mul_zero]},
+  { rw [ring.inverse_non_unit _ hab, ring.inverse_non_unit _ hb, zero_mul]},
+end
+
+end ring
+
 variable (M₀)
 
 end monoid_with_zero
@@ -800,6 +854,16 @@ by simp only [div_eq_mul_inv, mul_inv_rev₀, mul_assoc, mul_inv_cancel_left₀
 lemma mul_mul_div (a : G₀) {b : G₀} (hb : b ≠ 0) : a = a * b * (1 / b) :=
 by simp [hb]
 
+lemma ring.inverse_eq_inv (a : G₀) : ring.inverse a = a⁻¹ :=
+begin
+  obtain rfl | ha := eq_or_ne a 0,
+  { simp },
+  { exact ring.inverse_unit (units.mk0 a ha) }
+end
+
+@[simp] lemma ring.inverse_eq_inv' : (ring.inverse : G₀ → G₀) = has_inv.inv :=
+funext ring.inverse_eq_inv
+
 end group_with_zero
 
 section comm_group_with_zero -- comm

src/algebra/ring/basic.lean

@@ -1033,61 +1033,6 @@ end comm_ring
 
 end is_domain
 
-namespace ring
-variables {M₀ : Type*} [monoid_with_zero M₀]
-open_locale classical
-
-/-- Introduce a function `inverse` on a monoid with zero `M₀`, which sends `x` to `x⁻¹` if `x` is
-invertible and to `0` otherwise.  This definition is somewhat ad hoc, but one needs a fully (rather
-than partially) defined inverse function for some purposes, including for calculus.
-
-Note that while this is in the `ring` namespace for brevity, it requires the weaker assumption
-`monoid_with_zero M₀` instead of `ring M₀`. -/
-noncomputable def inverse : M₀ → M₀ :=
-λ x, if h : is_unit x then ((h.unit⁻¹ : units M₀) : M₀) else 0
-
-/-- By definition, if `x` is invertible then `inverse x = x⁻¹`. -/
-@[simp] lemma inverse_unit (u : units M₀) : inverse (u : M₀) = (u⁻¹ : units M₀) :=
-begin
-  simp only [units.is_unit, inverse, dif_pos],
-  exact units.inv_unique rfl
-end
-
-/-- By definition, if `x` is not invertible then `inverse x = 0`. -/
-@[simp] lemma inverse_non_unit (x : M₀) (h : ¬(is_unit x)) : inverse x = 0 := dif_neg h
-
-lemma mul_inverse_cancel (x : M₀) (h : is_unit x) : x * inverse x = 1 :=
-by { rcases h with ⟨u, rfl⟩, rw [inverse_unit, units.mul_inv], }
-
-lemma inverse_mul_cancel (x : M₀) (h : is_unit x) : inverse x * x = 1 :=
-by { rcases h with ⟨u, rfl⟩, rw [inverse_unit, units.inv_mul], }
-
-lemma mul_inverse_cancel_right (x y : M₀) (h : is_unit x) : y * x * inverse x = y :=
-by rw [mul_assoc, mul_inverse_cancel x h, mul_one]
-
-lemma inverse_mul_cancel_right (x y : M₀) (h : is_unit x) : y * inverse x * x = y :=
-by rw [mul_assoc, inverse_mul_cancel x h, mul_one]
-
-lemma mul_inverse_cancel_left (x y : M₀) (h : is_unit x) : x * (inverse x * y) = y :=
-by rw [← mul_assoc, mul_inverse_cancel x h, one_mul]
-
-lemma inverse_mul_cancel_left (x y : M₀) (h : is_unit x) : inverse x * (x * y) = y :=
-by rw [← mul_assoc, inverse_mul_cancel x h, one_mul]
-
-lemma mul_inverse_rev {M₀ : Type*} [comm_monoid_with_zero M₀] (a b : M₀) :
-  ring.inverse (a * b) = ring.inverse b * ring.inverse a :=
-begin
-  by_cases hab : is_unit (a * b),
-  { obtain ⟨⟨a, rfl⟩, b, rfl⟩ := is_unit.mul_iff.mp hab,
-    rw [←units.coe_mul, ring.inverse_unit, ring.inverse_unit, ring.inverse_unit, ←units.coe_mul,
-      mul_inv_rev], },
-  obtain ha | hb := not_and_distrib.mp (mt is_unit.mul_iff.mpr hab),
-  { rw [ring.inverse_non_unit _ hab, ring.inverse_non_unit _ ha, mul_zero]},
-  { rw [ring.inverse_non_unit _ hab, ring.inverse_non_unit _ hb, zero_mul]},
-end
-
-end ring
-
 namespace semiconj_by
 
 @[simp] lemma add_right [distrib R] {a x y x' y' : R}

src/analysis/calculus/times_cont_diff.lean

@@ -2484,7 +2484,7 @@ variables (𝕜) {𝕜' : Type*} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'
 
 lemma times_cont_diff_at_inv {x : 𝕜'} (hx : x ≠ 0) {n} :
   times_cont_diff_at 𝕜 n has_inv.inv x :=
-by simpa only [inverse_eq_has_inv] using times_cont_diff_at_ring_inverse 𝕜 (units.mk0 x hx)
+by simpa only [ring.inverse_eq_inv'] using times_cont_diff_at_ring_inverse 𝕜 (units.mk0 x hx)
 
 lemma times_cont_diff_on_inv {n} : times_cont_diff_on 𝕜 n (has_inv.inv : 𝕜' → 𝕜') {0}ᶜ :=
 λ x hx, (times_cont_diff_at_inv 𝕜 hx).times_cont_diff_within_at