chore(algebra/*): merge inv_inv'' with inv_inv' (#2954)

src/algebra/field.lean

@@ -172,9 +172,6 @@ match classical.em (a = 0) with
 | or.inr h := eq.symm (eq_one_div_of_mul_eq_one_left (mul_one_div_cancel h))
 end
 
-lemma inv_inv' (a : α) : a⁻¹⁻¹ = a :=
-by rw [inv_eq_one_div, inv_eq_one_div, one_div_one_div]
-
 lemma eq_of_one_div_eq_one_div (h : 1 / a = 1 / b) : a = b :=
 by rw [← one_div_one_div a, h,one_div_one_div]
 

src/algebra/group_with_zero.lean

@@ -110,7 +110,7 @@ calc (a * b⁻¹) * b = a * (b⁻¹ * b) : mul_assoc _ _ _
 calc a⁻¹ * (a * b) = (a⁻¹ * a) * b : (mul_assoc _ _ _).symm
                ... = b             : by simp [h]
 
-@[simp] lemma inv_inv'' (a : G₀) : a⁻¹⁻¹ = a :=
+@[simp] lemma inv_inv' (a : G₀) : a⁻¹⁻¹ = a :=
 begin
   classical,
   by_cases h : a = 0, { simp [h] },
@@ -159,7 +159,7 @@ mul_self_mul_inv a
 mul_inv_mul_self a
 
 lemma inv_involutive' : function.involutive (has_inv.inv : G₀ → G₀) :=
-inv_inv''
+inv_inv'
 
 lemma ne_zero_of_mul_right_eq_one' (a b : G₀) (h : a * b = 1) : a ≠ 0 :=
 assume a_eq_0, zero_ne_one (by simpa [a_eq_0] using h : (0:G₀) = 1)
@@ -189,7 +189,7 @@ inv_involutive'.injective
 ⟨assume H, inv_injective' H, congr_arg _⟩
 
 lemma inv_eq_iff {g h : G₀} : g⁻¹ = h ↔ h⁻¹ = g :=
-by rw [← inv_inj'', eq_comm, inv_inv'']
+by rw [← inv_inj'', eq_comm, inv_inv']
 
 @[simp] lemma coe_unit_mul_inv' (a : units G₀) : (a : G₀) * a⁻¹ = 1 :=
 mul_inv_cancel' _ $ ne_zero_of_mul_right_eq_one' _ (a⁻¹ : units G₀) $ by simp
@@ -361,7 +361,7 @@ have a ≠ 0, from
 by rw [← h, mul_div_assoc'', div_self' this, mul_one]
 
 @[simp] lemma one_div_div' (a b : G₀) : 1 / (a / b) = b / a :=
-by rw [one_div, div_eq_mul_inv, mul_inv_rev', inv_inv'', div_eq_mul_inv]
+by rw [one_div, div_eq_mul_inv, mul_inv_rev', inv_inv', div_eq_mul_inv]
 
 @[simp] lemma one_div_one_div' (a : G₀) : 1 / (1 / a) = a :=
 by simp
@@ -390,7 +390,7 @@ congr_arg _ $ units.inv_eq_inv _
 divp_eq_div _ _
 
 lemma inv_div : (a / b)⁻¹ = b / a :=
-(mul_inv_rev' _ _).trans (by rw inv_inv''; refl)
+(mul_inv_rev' _ _).trans (by rw inv_inv'; refl)
 
 lemma inv_div_left : a⁻¹ / b = (b * a)⁻¹ :=
 (mul_inv_rev' _ _).symm
@@ -409,7 +409,7 @@ lemma div_left_inj' (hc : c ≠ 0) : a / c = b / c ↔ a = b :=
 by rw [← divp_mk0 _ hc, ← divp_mk0 _ hc, divp_left_inj]
 
 lemma mul_left_inj' (hc : c ≠ 0) : a * c = b * c ↔ a = b :=
-by rw [← inv_inv'' c, ← div_eq_mul_inv, ← div_eq_mul_inv, div_left_inj' (inv_ne_zero' hc)]
+by rw [← inv_inv' c, ← div_eq_mul_inv, ← div_eq_mul_inv, div_left_inj' (inv_ne_zero' hc)]
 
 lemma div_eq_iff_mul_eq (hb : b ≠ 0) : a / b = c ↔ c * b = a :=
 ⟨λ h, by rw [← h, div_mul_cancel' _ hb],

src/algebra/group_with_zero_power.lean

@@ -87,7 +87,7 @@ lemma zero_fpow : ∀ z : ℤ, z ≠ 0 → (0 : G₀) ^ z = 0
 @[simp] theorem fpow_neg (a : G₀) : ∀ (n : ℤ), a ^ -n = (a ^ n)⁻¹
 | (n+1:ℕ) := rfl
 | 0       := inv_one'.symm
-| -[1+ n] := (inv_inv'' _).symm
+| -[1+ n] := (inv_inv' _).symm
 
 theorem fpow_neg_one (x : G₀) : x ^ (-1:ℤ) = x⁻¹ := congr_arg has_inv.inv $ pow_one x
 
@@ -103,7 +103,7 @@ or.elim (nat.lt_or_ge m (nat.succ n))
   suffices a ^ -[1+ n-m] = a ^ of_nat m * a ^ -[1+n],
     by rwa [of_nat_add_neg_succ_of_nat_of_lt h1],
   show (a ^ nat.succ (n - m))⁻¹ = a ^ of_nat m * a ^ -[1+n],
-  by rw [← nat.succ_sub h2, pow_sub' _ h (le_of_lt h1), mul_inv_rev', inv_inv'']; refl)
+  by rw [← nat.succ_sub h2, pow_sub' _ h (le_of_lt h1), mul_inv_rev', inv_inv']; refl)
  (assume : m ≥ n.succ,
   suffices a ^ (of_nat (m - n.succ)) = (a ^ (of_nat m)) * (a ^ -[1+ n]),
     by rw [of_nat_add_neg_succ_of_nat_of_ge]; assumption,
@@ -135,7 +135,7 @@ theorem fpow_mul (a : G₀) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n
 | -[1+ m] (n : ℕ) := (fpow_neg _ (m.succ * n)).trans $
   show (a ^ (m.succ * n))⁻¹ = _, by rw [pow_mul, ← inv_pow']; refl
 | -[1+ m] -[1+ n] := (pow_mul a m.succ n.succ).trans $
-  show _ = (_⁻¹ ^ _)⁻¹, by rw [inv_pow', inv_inv'']
+  show _ = (_⁻¹ ^ _)⁻¹, by rw [inv_pow', inv_inv']
 
 theorem fpow_mul' (a : G₀) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m :=
 by rw [mul_comm, fpow_mul]

src/algebra/ordered_field.lean

@@ -440,12 +440,12 @@ lemma div_pos : 0 < a → 0 < b → 0 < a / b := div_pos_of_pos_of_pos
 
 @[simp] lemma inv_pos : ∀ {a : α}, 0 < a⁻¹ ↔ 0 < a :=
 suffices ∀ a : α, 0 < a → 0 < a⁻¹,
-from λ a, ⟨λ h, inv_inv'' a ▸ this _ h, this a⟩,
+from λ a, ⟨λ h, inv_inv' a ▸ this _ h, this a⟩,
 λ a, one_div_eq_inv a ▸ one_div_pos_of_pos
 
 @[simp] lemma inv_lt_zero : ∀ {a : α}, a⁻¹ < 0 ↔ a < 0 :=
 suffices ∀ a : α, a < 0 → a⁻¹ < 0,
-from λ a, ⟨λ h, inv_inv'' a ▸ this _ h, this a⟩,
+from λ a, ⟨λ h, inv_inv' a ▸ this _ h, this a⟩,
 λ a, one_div_eq_inv a ▸ one_div_neg_of_neg
 
 @[simp] lemma inv_nonneg : 0 ≤ a⁻¹ ↔ 0 ≤ a :=

src/algebra/pointwise.lean

@@ -332,7 +332,7 @@ iff.intro
 
 lemma mem_smul_set_iff_inv_smul_mem [field α] [mul_action α β]
   {a : α} (ha : a ≠ 0) (A : set β) (x : β) : x ∈ a • A ↔ a⁻¹ • x ∈ A :=
-by conv_lhs { rw ← inv_inv'' a };
+by conv_lhs { rw ← inv_inv' a };
    exact (mem_inv_smul_set_iff (inv_ne_zero ha) _ _)
 
 end