refactor(algebra/group/basic): add extra typeclasses for negation (#1…

…1960)

The new typeclasses are:
* `has_involutive_inv R`, stating that `(r⁻¹)⁻¹ = r`  
  (instances: `group`, `group_with_zero`, `ennreal`, `set`, `submonoid`)
* `has_involutive_neg R`, stating that `- -r = r`
  (instances: `add_group`, `ereal`, `module.ray`, `ray_vector`, `set`, `add_submonoid`, `jordan_decomposition`)
* `has_distrib_neg R`, stating that `-a * b = a * -b = -(a * b)`
  (instances: `ring`, `units`, `unitary`, `special_linear_group`, `GL_pos`)

While the original motivation only concerned the two `neg` typeclasses, the `to_additive` machinery forced the introduction of `has_involutive_inv`, which turned out to be used in more places than expected.

Adding these typeclases removes a large number of specialized `units R` lemmas as the lemmas about `R` now match themselves. A surprising number of lemmas elsewhere in the library can also be removed. The removed lemmas are:
* Lemmas about `units` (replaced by `units.has_distrib_neg`):
  * `units.neg_one_pow_eq_or`
  * `units.neg_pow`
  * `units.neg_pow_bit0`
  * `units.neg_pow_bit1`
  * `units.neg_sq`
  * `units.neg_inv` (now `inv_neg'` for arbitrary groups with distributive negation)
  * `units.neg_neg`
  * `units.neg_mul`
  * `units.mul_neg`
  * `units.neg_mul_eq_neg_mul`
  * `units.neg_mul_eq_mul_neg`
  * `units.neg_mul_neg`
  * `units.neg_eq_neg_one_mul`
  * `units.mul_neg_one`
  * `units.neg_one_mul`
  * `semiconj_by.units_neg_right`
  * `semiconj_by.units_neg_right_iff`
  * `semiconj_by.units_neg_left`
  * `semiconj_by.units_neg_left_iff`
  * `semiconj_by.units_neg_one_right`
  * `semiconj_by.units_neg_one_left`
  * `commute.units_neg_right`
  * `commute.units_neg_right_iff`
  * `commute.units_neg_left`
  * `commute.units_neg_left_iff`
  * `commute.units_neg_one_right`
  * `commute.units_neg_one_left`
* Lemmas about groups with zero (replaced by `group_with_zero.to_has_involutive_neg`):
  * `inv_inv₀`
  * `inv_involutive₀`
  * `inv_injective₀`
  * `inv_eq_iff` (now shared with the `inv_eq_iff_inv_eq` group lemma)
  * `eq_inv_iff` (now shared with the `eq_inv_iff_eq_inv` group lemma)
  * `equiv.inv₀`
  * `measurable_equiv.inv₀`
* Lemmas about `ereal` (replaced by `ereal.has_involutive_neg`):
  * `ereal.neg_neg`
  * `ereal.neg_inj`
  * `ereal.neg_eq_neg_iff`
  * `ereal.neg_eq_iff_neg_eq`
* Lemmas about `ennreal` (replaced by `ennreal.has_involutive_inv`):
  * `ereal.inv_inv`
  * `ereal.inv_involutive`
  * `ereal.inv_bijective`
  * `ereal.inv_eq_inv`
* Other lemmas:
  * `ray_vector.neg_neg`
  * `module.ray.neg_neg`
  * `module.ray.neg_involutive`
  * `module.ray.eq_neg_iff_eq_neg`
  * `set.inv_inv`
  * `set.neg_neg`
  * `submonoid.inv_inv`
  * `add_submonoid.neg_neg`

As a bonus, this provides the group `unitary R`  with a negation operator and all the lemmas listed for `units` above.

For now this doesn't attempt to unify `units.neg_smul` and `neg_smul`.

src/algebra/group/basic.lean

@@ -150,6 +150,36 @@ eq_comm.trans mul_left_eq_self
 
 end right_cancel_monoid
 
+section has_involutive_inv
+variables {G : Type u} [has_involutive_inv G] {a b : G}
+
+@[simp, to_additive]
+lemma inv_involutive : function.involutive (has_inv.inv : G → G) := inv_inv
+
+@[simp, to_additive]
+lemma inv_surjective : function.surjective (has_inv.inv : G → G) :=
+inv_involutive.surjective
+
+@[to_additive]
+lemma inv_injective : function.injective (has_inv.inv : G → G) :=
+inv_involutive.injective
+
+@[simp, to_additive] theorem inv_inj {a b : G} : a⁻¹ = b⁻¹ ↔ a = b := inv_injective.eq_iff
+
+@[to_additive]
+lemma eq_inv_of_eq_inv (h : a = b⁻¹) : b = a⁻¹ :=
+by simp [h]
+
+@[to_additive]
+theorem eq_inv_iff_eq_inv : a = b⁻¹ ↔ b = a⁻¹ :=
+⟨eq_inv_of_eq_inv, eq_inv_of_eq_inv⟩
+
+@[to_additive]
+theorem inv_eq_iff_inv_eq  : a⁻¹ = b ↔ b⁻¹ = a :=
+eq_comm.trans $ eq_inv_iff_eq_inv.trans eq_comm
+
+end has_involutive_inv
+
 section div_inv_monoid
 
 variables {G : Type u} [div_inv_monoid G]
@@ -193,19 +223,6 @@ theorem left_inverse_inv (G) [group G] :
   function.left_inverse (λ a : G, a⁻¹) (λ a, a⁻¹) :=
 inv_inv
 
-@[simp, to_additive]
-lemma inv_involutive : function.involutive (has_inv.inv : G → G) := inv_inv
-
-@[simp, to_additive]
-lemma inv_surjective : function.surjective (has_inv.inv : G → G) :=
-inv_involutive.surjective
-
-@[to_additive]
-lemma inv_injective : function.injective (has_inv.inv : G → G) :=
-inv_involutive.injective
-
-@[simp, to_additive] theorem inv_inj : a⁻¹ = b⁻¹ ↔ a = b := inv_injective.eq_iff
-
 @[simp, to_additive]
 theorem inv_eq_one : a⁻¹ = 1 ↔ a = 1 := inv_injective.eq_iff' one_inv
 
@@ -234,10 +251,6 @@ theorem mul_right_surjective (a : G) : function.surjective (λ x, x * a) :=
 lemma mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
 inv_eq_of_mul_eq_one $ by simp
 
-@[to_additive]
-lemma eq_inv_of_eq_inv (h : a = b⁻¹) : b = a⁻¹ :=
-by simp [h]
-
 @[to_additive]
 lemma eq_inv_of_mul_eq_one (h : a * b = 1) : a = b⁻¹ :=
 have a⁻¹ = b, from inv_eq_of_mul_eq_one h,
@@ -275,14 +288,6 @@ by rw [h, mul_inv_cancel_left]
 lemma mul_eq_of_eq_mul_inv (h : a = c * b⁻¹) : a * b = c :=
 by simp [h]
 
-@[to_additive]
-theorem eq_inv_iff_eq_inv : a = b⁻¹ ↔ b = a⁻¹ :=
-⟨eq_inv_of_eq_inv, eq_inv_of_eq_inv⟩
-
-@[to_additive]
-theorem inv_eq_iff_inv_eq : a⁻¹ = b ↔ b⁻¹ = a :=
-eq_comm.trans $ eq_inv_iff_eq_inv.trans eq_comm
-
 @[to_additive]
 theorem mul_eq_one_iff_eq_inv : a * b = 1 ↔ a = b⁻¹ :=
 ⟨eq_inv_of_mul_eq_one, λ h, by rw [h, mul_left_inv]⟩

src/algebra/group/defs.lean

@@ -595,6 +595,33 @@ lemma div_eq_mul_inv {G : Type u} [div_inv_monoid G] :
   ∀ a b : G, a / b = a * b⁻¹ :=
 div_inv_monoid.div_eq_mul_inv
 
+section
+-- ensure that we don't go via these typeclasses to find `has_inv` on groups and groups with zero
+set_option extends_priority 50
+
+/-- Auxiliary typeclass for types with an involutive `has_inv`. -/
+@[ancestor has_inv]
+class has_involutive_inv (G : Type*) extends has_inv G :=
+(inv_inv : ∀ x : G, x⁻¹⁻¹ = x)
+
+/-- Auxiliary typeclass for types with an involutive `has_neg`. -/
+@[ancestor has_neg]
+class has_involutive_neg (A : Type*) extends has_neg A :=
+(neg_neg : ∀ x : A, - -x = x)
+
+attribute [to_additive] has_involutive_inv
+
+end
+
+section has_involutive_inv
+variables {G : Type*} [has_involutive_inv G]
+
+@[simp, to_additive]
+lemma inv_inv (a : G) : (a⁻¹)⁻¹ = a :=
+has_involutive_inv.inv_inv _
+
+end has_involutive_inv
+
 /-- A `group` is a `monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.
 
 There is also a division operation `/` such that `a / b = a * b⁻¹`,
@@ -646,9 +673,10 @@ by rw [← mul_assoc, mul_left_inv, one_mul]
 lemma inv_eq_of_mul_eq_one (h : a * b = 1) : a⁻¹ = b :=
 left_inv_eq_right_inv (inv_mul_self a) h
 
-@[simp, to_additive]
-lemma inv_inv (a : G) : (a⁻¹)⁻¹ = a :=
-inv_eq_of_mul_eq_one (mul_left_inv a)
+@[priority 100, to_additive]
+instance group.to_has_involutive_inv : has_involutive_inv G :=
+{ inv := has_inv.inv,
+  inv_inv := λ a, inv_eq_of_mul_eq_one (mul_left_inv a) }
 
 @[simp, to_additive]
 lemma mul_right_inv (a : G) : a * a⁻¹ = 1 :=

src/algebra/group_power/basic.lean

@@ -346,26 +346,16 @@ alias add_sq ← add_pow_two
 
 end comm_semiring
 
-section ring
-variable [ring R]
+section has_distrib_neg
+variables [monoid R] [has_distrib_neg R]
 
-section
 variables (R)
 theorem neg_one_pow_eq_or : ∀ n : ℕ, (-1 : R)^n = 1 ∨ (-1 : R)^n = -1
 | 0     := or.inl (pow_zero _)
 | (n+1) := (neg_one_pow_eq_or n).swap.imp
   (λ h, by rw [pow_succ, h, neg_one_mul, neg_neg])
   (λ h, by rw [pow_succ, h, mul_one])
-
-end
-
-@[simp]
-lemma neg_one_pow_mul_eq_zero_iff {n : ℕ} {r : R} : (-1)^n * r = 0 ↔ r = 0 :=
-by rcases neg_one_pow_eq_or R n; simp [h]
-
-@[simp]
-lemma mul_neg_one_pow_eq_zero_iff {n : ℕ} {r : R} : r * (-1)^n = 0 ↔ r = 0 :=
-by rcases neg_one_pow_eq_or R n; simp [h]
+variables {R}
 
 theorem neg_pow (a : R) (n : ℕ) : (- a) ^ n = (-1) ^ n * a ^ n :=
 (neg_one_mul a) ▸ (commute.neg_one_left a).mul_pow n
@@ -381,32 +371,18 @@ by simp [sq]
 
 alias neg_sq ← neg_pow_two
 
-/- Copies of the above ring lemmas for `units R`. -/
-namespace units
-
-section
-variables (R)
-theorem neg_one_pow_eq_or : ∀ n : ℕ, (-1 : Rˣ)^n = 1 ∨ (-1 : Rˣ)^n = -1
-| 0     := or.inl (pow_zero _)
-| (n+1) := (neg_one_pow_eq_or n).swap.imp
-  (λ h, by rw [pow_succ, h, ←units.neg_eq_neg_one_mul, units.neg_neg])
-  (λ h, by rw [pow_succ, h, mul_one])
-
-end
-
-theorem neg_pow (a : Rˣ) (n : ℕ) : (- a) ^ n = (-1) ^ n * a ^ n :=
-(units.neg_eq_neg_one_mul a).symm ▸ (commute.units_neg_one_left a).mul_pow n
-
-@[simp] theorem neg_pow_bit0 (a : Rˣ) (n : ℕ) : (- a) ^ (bit0 n) = a ^ (bit0 n) :=
-by rw [pow_bit0', units.neg_mul_neg, pow_bit0']
+end has_distrib_neg
 
-@[simp] theorem neg_pow_bit1 (a : Rˣ) (n : ℕ) : (- a) ^ (bit1 n) = - a ^ (bit1 n) :=
-by simp only [bit1, pow_succ, neg_pow_bit0, units.neg_mul_eq_neg_mul]
+section ring
+variable [ring R]
 
-@[simp] lemma neg_sq (a : Rˣ) : (-a)^2 = a^2 :=
-by simp [sq]
+@[simp]
+lemma neg_one_pow_mul_eq_zero_iff {n : ℕ} {r : R} : (-1)^n * r = 0 ↔ r = 0 :=
+by rcases neg_one_pow_eq_or R n; simp [h]
 
-end units
+@[simp]
+lemma mul_neg_one_pow_eq_zero_iff {n : ℕ} {r : R} : r * (-1)^n = 0 ↔ r = 0 :=
+by rcases neg_one_pow_eq_or R n; simp [h]
 
 end ring
 

src/algebra/group_with_zero/basic.lean

@@ -576,12 +576,14 @@ calc a⁻¹ * (a * b) = (a⁻¹ * a) * b : (mul_assoc _ _ _).symm
 calc 1⁻¹ = 1 * 1⁻¹ : by rw [one_mul]
      ... = (1:G₀)  : by simp
 
-@[simp] lemma inv_inv₀ (a : G₀) : a⁻¹⁻¹ = a :=
-begin
-  by_cases h : a = 0, { simp [h] },
-  calc a⁻¹⁻¹ = a * (a⁻¹ * a⁻¹⁻¹) : by simp [h]
-         ... = a                 : by simp [inv_ne_zero h]
-end
+@[priority 100]
+instance group_with_zero.to_has_involutive_inv : has_involutive_inv G₀ :=
+{ inv := has_inv.inv,
+  inv_inv := λ a, begin
+    by_cases h : a = 0, { simp [h] },
+    calc a⁻¹⁻¹ = a * (a⁻¹ * a⁻¹⁻¹) : by simp [h]
+          ... = a                 : by simp [inv_ne_zero h]
+  end }
 
 /-- Multiplying `a` by itself and then by its inverse results in `a`
 (whether or not `a` is zero). -/
@@ -620,9 +622,6 @@ by rw [div_eq_mul_inv, mul_self_mul_inv a]
 @[simp] lemma div_self_mul_self (a : G₀) : a / a * a = a :=
 by rw [div_eq_mul_inv, mul_inv_mul_self a]
 
-lemma inv_involutive₀ : function.involutive (has_inv.inv : G₀ → G₀) :=
-inv_inv₀
-
 lemma eq_inv_of_mul_right_eq_one (h : a * b = 1) :
   b = a⁻¹ :=
 by rw [← inv_mul_cancel_left₀ (left_ne_zero_of_mul_eq_one h) b, h, mul_one]
@@ -631,23 +630,8 @@ lemma eq_inv_of_mul_left_eq_one (h : a * b = 1) :
   a = b⁻¹ :=
 by rw [← mul_inv_cancel_right₀ (right_ne_zero_of_mul_eq_one h) a, h, one_mul]
 
-lemma inv_injective₀ : function.injective (@has_inv.inv G₀ _) :=
-inv_involutive₀.injective
-
-@[simp] lemma inv_inj₀ : g⁻¹ = h⁻¹ ↔ g = h := inv_injective₀.eq_iff
-
-/-- This is the analogue of `inv_eq_iff_inv_eq` for `group_with_zero`.
-  It could also be named `inv_eq_iff_inv_eq'`. -/
-lemma inv_eq_iff : g⁻¹ = h ↔ h⁻¹ = g :=
-by rw [← inv_inj₀, eq_comm, inv_inv₀]
-
-/-- This is the analogue of `eq_inv_iff_eq_inv` for `group_with_zero`.
-  It could also be named `eq_inv_iff_eq_inv'`. -/
-lemma eq_inv_iff : a = b⁻¹ ↔ b = a⁻¹ :=
-by rw [eq_comm, inv_eq_iff, eq_comm]
-
 @[simp] lemma inv_eq_one₀ : g⁻¹ = 1 ↔ g = 1 :=
-by rw [inv_eq_iff, inv_one, eq_comm]
+by rw [inv_eq_iff_inv_eq, inv_one, eq_comm]
 
 lemma eq_mul_inv_iff_mul_eq₀ (hc : c ≠ 0) : a = b * c⁻¹ ↔ a * c = b :=
 by split; rintro rfl; [rw inv_mul_cancel_right₀ hc, rw mul_inv_cancel_right₀ hc]
@@ -668,10 +652,10 @@ lemma inv_mul_eq_one₀ (ha : a ≠ 0) : a⁻¹ * b = 1 ↔ a = b :=
 by rw [inv_mul_eq_iff_eq_mul₀ ha, mul_one, eq_comm]
 
 lemma mul_eq_one_iff_eq_inv₀ (hb : b ≠ 0) : a * b = 1 ↔ a = b⁻¹ :=
-by { convert mul_inv_eq_one₀ (inv_ne_zero hb), rw [inv_inv₀] }
+by { convert mul_inv_eq_one₀ (inv_ne_zero hb), rw [inv_inv] }
 
 lemma mul_eq_one_iff_inv_eq₀ (ha : a ≠ 0) : a * b = 1 ↔ a⁻¹ = b :=
-by { convert inv_mul_eq_one₀ (inv_ne_zero ha), rw [inv_inv₀] }
+by { convert inv_mul_eq_one₀ (inv_ne_zero ha), rw [inv_inv] }
 
 end group_with_zero
 
@@ -814,7 +798,7 @@ lemma eq_one_div_of_mul_eq_one_left {a b : G₀} (h : b * a = 1) : b = 1 / a :=
 by simpa only [one_div] using eq_inv_of_mul_left_eq_one h
 
 @[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]
 
 lemma one_div_one_div (a : G₀) : 1 / (1 / a) = a :=
 by simp
@@ -825,7 +809,7 @@ by rw [← one_div_one_div a, h, one_div_one_div]
 variables {a b c : G₀}
 
 @[simp] lemma inv_eq_zero {a : G₀} : a⁻¹ = 0 ↔ a = 0 :=
-by rw [inv_eq_iff, inv_zero, eq_comm]
+by rw [inv_eq_iff_inv_eq, inv_zero, eq_comm]
 
 @[simp] lemma zero_eq_inv {a : G₀} : 0 = a⁻¹ ↔ 0 = a :=
 eq_comm.trans $ inv_eq_zero.trans eq_comm
@@ -841,7 +825,7 @@ by simpa only [div_eq_mul_inv] using congr_arg ((*) a) u.coe_inv'
 divp_eq_div _ _
 
 lemma inv_div : (a / b)⁻¹ = b / a :=
-by rw [div_eq_mul_inv, mul_inv_rev₀, div_eq_mul_inv, inv_inv₀]
+by rw [div_eq_mul_inv, mul_inv_rev₀, div_eq_mul_inv, inv_inv]
 
 lemma inv_div_left : a⁻¹ / b = (b * a)⁻¹ :=
 by rw [mul_inv_rev₀, div_eq_mul_inv]
@@ -1086,7 +1070,7 @@ begin
 end
 
 @[simp] lemma inv_right_iff₀ : semiconj_by a x⁻¹ y⁻¹ ↔ semiconj_by a x y :=
-⟨λ h, inv_inv₀ x ▸ inv_inv₀ y ▸ h.inv_right₀, inv_right₀⟩
+⟨λ h, inv_inv x ▸ inv_inv y ▸ h.inv_right₀, inv_right₀⟩
 
 lemma div_right (h : semiconj_by a x y) (h' : semiconj_by a x' y') :
   semiconj_by a (x / x') (y / y') :=

src/algebra/group_with_zero/power.lean

@@ -64,10 +64,10 @@ theorem pow_inv_comm₀ (a : G₀) (m n : ℕ) : (a⁻¹) ^ m * a ^ n = a ^ n *
 (commute.refl a).inv_left₀.pow_pow m n
 
 lemma inv_pow_sub₀ (ha : a ≠ 0) (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n :=
-by rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow₀, inv_pow₀, inv_inv₀]
+by rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow₀, inv_pow₀, inv_inv]
 
 lemma inv_pow_sub_of_lt (a : G₀) (h : n < m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n :=
-by rw [pow_sub_of_lt a⁻¹ h, inv_pow₀, inv_pow₀, inv_inv₀]
+by rw [pow_sub_of_lt a⁻¹ h, inv_pow₀, inv_pow₀, inv_inv]
 
 end nat_pow
 
@@ -97,7 +97,7 @@ end
 @[simp] theorem zpow_neg₀ (a : G₀) : ∀ (n : ℤ), a ^ -n = (a ^ n)⁻¹
 | (n+1:ℕ) := div_inv_monoid.zpow_neg' _ _
 | 0       := by { change a ^ (0 : ℤ) = (a ^ (0 : ℤ))⁻¹, simp }
-| -[1+ n] := by { rw [zpow_neg_succ_of_nat, inv_inv₀, ← zpow_coe_nat], refl }
+| -[1+ n] := by { rw [zpow_neg_succ_of_nat, inv_inv, ← zpow_coe_nat], refl }
 
 lemma mul_zpow_neg_one₀ (a b : G₀) : (a * b) ^ (-1 : ℤ) = b ^ (-1 : ℤ) * a ^ (-1 : ℤ) :=
 by simp only [mul_inv_rev₀, zpow_one, zpow_neg₀]
@@ -182,11 +182,11 @@ end
 theorem zpow_mul₀ (a : G₀) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n
 | (m : ℕ) (n : ℕ) := by { rw [zpow_coe_nat, zpow_coe_nat, ← pow_mul, ← zpow_coe_nat], refl }
 | (m : ℕ) -[1+ n] := by { rw [zpow_coe_nat, zpow_neg_succ_of_nat, ← pow_mul, coe_nat_mul_neg_succ,
-    zpow_neg₀, inv_inj₀, ← zpow_coe_nat], refl }
+    zpow_neg₀, inv_inj, ← zpow_coe_nat], refl }
 | -[1+ m] (n : ℕ) := by { rw [zpow_coe_nat, zpow_neg_succ_of_nat, ← inv_pow₀, ← pow_mul,
-    neg_succ_mul_coe_nat, zpow_neg₀, inv_pow₀, inv_inj₀, ← zpow_coe_nat], refl }
+    neg_succ_mul_coe_nat, zpow_neg₀, inv_pow₀, inv_inj, ← zpow_coe_nat], refl }
 | -[1+ m] -[1+ n] := by { rw [zpow_neg_succ_of_nat, zpow_neg_succ_of_nat, neg_succ_mul_neg_succ,
-    inv_pow₀, inv_inv₀, ← pow_mul, ← zpow_coe_nat], refl }
+    inv_pow₀, inv_inv, ← pow_mul, ← zpow_coe_nat], refl }
 
 theorem zpow_mul₀' (a : G₀) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m :=
 by rw [mul_comm, zpow_mul₀]