feat(algebra/ring): units.neg and associated matter

algebra/group.lean

@@ -189,59 +189,82 @@ structure units (α : Type u) [monoid α] :=
 (inv_val : inv * val = 1)
 
 namespace units
-  variables [monoid α] {a b c : units α}
+variables [monoid α] {a b c : units α}
 
-  instance : has_coe (units α) α := ⟨val⟩
+instance : has_coe (units α) α := ⟨val⟩
 
-  theorem ext : ∀ {a b : units α}, (a : α) = b → a = b
-  | ⟨v, i₁, vi₁, iv₁⟩ ⟨v', i₂, vi₂, iv₂⟩ e :=
-    by change v = v' at e; subst v'; congr;
-       simpa [iv₂, vi₁] using mul_assoc i₂ v i₁
+@[extensionality] theorem ext : ∀ {a b : units α}, (a : α) = b → a = b
+| ⟨v, i₁, vi₁, iv₁⟩ ⟨v', i₂, vi₂, iv₂⟩ e :=
+  by change v = v' at e; subst v'; congr;
+      simpa [iv₂, vi₁] using mul_assoc i₂ v i₁
 
-  protected def mul : units α → units α → units α
-  | ⟨v₁, i₁, vi₁, iv₁⟩ ⟨v₂, i₂, vi₂, iv₂⟩ := ⟨v₁ * v₂, i₂ * i₁,
-    have v₁ * (v₂ * i₂) * i₁ = 1, by rw [vi₂]; simp [vi₁], by simpa [mul_comm, mul_assoc],
-    have i₂ * (i₁ * v₁) * v₂ = 1, by rw [iv₁]; simp [iv₂], by simpa [mul_comm, mul_assoc]⟩
+theorem ext_iff {a b : units α} : a = b ↔ (a : α) = b :=
+⟨congr_arg _, ext⟩
 
-  protected def inv' : units α → units α
-  | ⟨v, i, vi, iv⟩ := ⟨i, v, iv, vi⟩
+instance [decidable_eq α] : decidable_eq (units α)
+| a b := decidable_of_iff' _ ext_iff
 
-  instance : has_mul (units α) := ⟨units.mul⟩
-  instance : has_one (units α) := ⟨⟨1, 1, mul_one 1, one_mul 1⟩⟩
-  instance : has_inv (units α) := ⟨units.inv'⟩
+protected def mul (u₁ u₂ : units α) : units α :=
+⟨u₁.val * u₂.val, u₂.inv * u₁.inv,
+  have u₁.val * (u₂.val * u₂.inv) * u₁.inv = 1,
+    by rw [u₂.val_inv]; simp [u₁.val_inv],
+  by simpa [mul_comm, mul_assoc],
+  have u₂.inv * (u₁.inv * u₁.val) * u₂.val = 1,
+    by rw [u₁.inv_val]; simp [u₂.inv_val],
+  by simpa [mul_comm, mul_assoc]⟩
 
-  variables (a b)
-  @[simp] lemma mul_coe : (↑(a * b) : α) = a * b := by cases a; cases b; refl
-  @[simp] lemma one_coe : ((1 : units α) : α) = 1 := rfl
-  lemma val_coe : (↑a : α) = a.val := rfl
-  lemma inv_coe : ((a⁻¹ : units α) : α) = a.inv := by cases a; refl
-  @[simp] lemma inv_mul : (↑a⁻¹ * a : α) = 1 := by simp [val_coe, inv_coe, inv_val]
-  @[simp] lemma mul_inv : (a * ↑a⁻¹ : α) = 1 := by simp [val_coe, inv_coe, val_inv]
+protected def inv' (u : units α) : units α :=
+⟨u.inv, u.val, u.inv_val, u.val_inv⟩
 
-  @[simp] lemma mul_inv_cancel_left (a : units α) (b : α) : (a:α) * (↑a⁻¹ * b) = b :=
-  by rw [← mul_assoc, mul_inv, one_mul]
+instance : has_mul (units α) := ⟨units.mul⟩
+instance : has_one (units α) := ⟨⟨1, 1, mul_one 1, one_mul 1⟩⟩
+instance : has_inv (units α) := ⟨units.inv'⟩
 
-  @[simp] lemma inv_mul_cancel_left (a : units α) (b : α) : (↑a⁻¹:α) * (a * b) = b :=
-  by rw [← mul_assoc, inv_mul, one_mul]
+variables (a b)
+@[simp] lemma mul_coe : (↑(a * b) : α) = a * b := rfl
+@[simp] lemma one_coe : ((1 : units α) : α) = 1 := rfl
+lemma val_coe : (↑a : α) = a.val := rfl
+lemma inv_coe : ((a⁻¹ : units α) : α) = a.inv := rfl
+@[simp] lemma inv_mul : (↑a⁻¹ * a : α) = 1 := inv_val _
+@[simp] lemma mul_inv : (a * ↑a⁻¹ : α) = 1 := val_inv _
 
-  @[simp] lemma mul_inv_cancel_right (a : α) (b : units α) : a * b * ↑b⁻¹ = a :=
-  by rw [mul_assoc, mul_inv, mul_one]
+@[simp] lemma mul_inv_cancel_left (a : units α) (b : α) : (a:α) * (↑a⁻¹ * b) = b :=
+by rw [← mul_assoc, mul_inv, one_mul]
 
-  @[simp] lemma inv_mul_cancel_right (a : α) (b : units α) : a * ↑b⁻¹ * b = a :=
-  by rw [mul_assoc, inv_mul, mul_one]
+@[simp] lemma inv_mul_cancel_left (a : units α) (b : α) : (↑a⁻¹:α) * (a * b) = b :=
+by rw [← mul_assoc, inv_mul, one_mul]
 
-  instance : group (units α) :=
-  by refine {mul := (*), one := 1, inv := has_inv.inv, ..};
-    { intros, apply ext, simp [mul_assoc] }
+@[simp] lemma mul_inv_cancel_right (a : α) (b : units α) : a * b * ↑b⁻¹ = a :=
+by rw [mul_assoc, mul_inv, mul_one]
 
-  @[simp] theorem mul_left_inj (a : units α) {b c : α} : (a:α) * b = a * c ↔ b = c :=
-  ⟨λ h, by simpa using congr_arg ((*) ↑(a⁻¹ : units α)) h, congr_arg _⟩
+@[simp] lemma inv_mul_cancel_right (a : α) (b : units α) : a * ↑b⁻¹ * b = a :=
+by rw [mul_assoc, inv_mul, mul_one]
 
-  @[simp] theorem mul_right_inj (a : units α) {b c : α} : b * a = c * a ↔ b = c :=
-  ⟨λ h, by simpa using congr_arg (* ↑(a⁻¹ : units α)) h, congr_arg _⟩
+instance : group (units α) :=
+by refine {mul := (*), one := 1, inv := has_inv.inv, ..};
+  { intros, apply ext, simp [mul_assoc] }
+
+instance {α} [comm_monoid α] : comm_group (units α) :=
+{ mul_comm := λ u₁ u₂, ext $ mul_comm _ _, ..units.group }
+
+@[simp] theorem mul_left_inj (a : units α) {b c : α} : (a:α) * b = a * c ↔ b = c :=
+⟨λ h, by simpa using congr_arg ((*) ↑(a⁻¹ : units α)) h, congr_arg _⟩
+
+@[simp] theorem mul_right_inj (a : units α) {b c : α} : b * a = c * a ↔ b = c :=
+⟨λ h, by simpa using congr_arg (* ↑(a⁻¹ : units α)) h, congr_arg _⟩
 
 end units
 
+theorem nat.units_eq_one (u : units ℕ) : u = 1 :=
+units.ext begin
+  cases nat.eq_zero_or_pos u with h h,
+  { simpa [h] using u.inv_mul },
+  cases nat.eq_zero_or_pos ↑u⁻¹ with h' h',
+  { simpa [h'] using u.inv_mul },
+  refine le_antisymm _ h,
+  simpa using nat.mul_le_mul_left u h'
+end
+
 @[to_additive with_zero]
 def with_one (α) := option α
 

algebra/ordered_group.lean

@@ -135,6 +135,43 @@ add_pos' h h
 
 end ordered_comm_monoid
 
+namespace units
+
+instance [monoid α] [preorder α] : preorder (units α) :=
+{ le := λ a b, (a:α) ≤ b,
+  lt := λ a b, (a:α) < b,
+  le_refl := λ a, @le_refl α _ _,
+  le_trans := λ a b c, @le_trans α _ _ _ _,
+  lt_iff_le_not_le := λ a b, @lt_iff_le_not_le α _ _ _ }
+
+@[simp] theorem coe_le_coe [monoid α] [preorder α] {a b : units α} :
+  (a : α) ≤ b ↔ a ≤ b := iff.rfl
+
+@[simp] theorem coe_lt_coe [monoid α] [preorder α] {a b : units α} :
+  (a : α) < b ↔ a < b := iff.rfl
+
+instance [monoid α] [partial_order α] : partial_order (units α) :=
+{ le_antisymm := λ a b h₁ h₂, ext $ le_antisymm h₁ h₂, ..units.preorder }
+
+instance [monoid α] [linear_order α] : linear_order (units α) :=
+{ le_total := λ a b, @le_total α _ _ _, ..units.partial_order }
+
+instance [monoid α] [decidable_linear_order α] : decidable_linear_order (units α) :=
+{ decidable_le := by apply_instance,
+  decidable_lt := by apply_instance,
+  decidable_eq := by apply_instance,
+  ..units.linear_order }
+
+theorem max_coe [monoid α] [decidable_linear_order α] {a b : units α} :
+  (↑(max a b) : α) = max a b :=
+by by_cases a ≤ b; simp [max, h]
+
+theorem min_coe [monoid α] [decidable_linear_order α] {a b : units α} :
+  (↑(min a b) : α) = min a b :=
+by by_cases a ≤ b; simp [min, h]
+
+end units
+
 namespace with_zero
 open lattice
 

algebra/ring.lean

@@ -9,15 +9,40 @@ universes u v
 variable {α : Type u}
 
 section
-  variable [semiring α]
+variable [semiring α]
 
-  theorem mul_two (n : α) : n * 2 = n + n :=
-  (left_distrib n 1 1).trans (by simp)
+theorem mul_two (n : α) : n * 2 = n + n :=
+(left_distrib n 1 1).trans (by simp)
 
-  theorem bit0_eq_two_mul (n : α) : bit0 n = 2 * n :=
-  (two_mul _).symm
+theorem bit0_eq_two_mul (n : α) : bit0 n = 2 * n :=
+(two_mul _).symm
 end
 
+namespace units
+variables [ring α] {a b : α}
+
+instance : has_neg (units α) :=
+⟨λ u, ⟨-u.val, -u.inv, by simp [u.val_inv], by simp [u.inv_val]⟩⟩
+
+@[simp] protected theorem coe_neg (u : units α) : (↑-u : α) = -u := rfl
+
+@[simp] protected theorem neg_inv (u : units α) : (-u)⁻¹ = -u⁻¹ := rfl
+
+@[simp] protected theorem neg_neg (u : units α) : - -u = u :=
+units.ext $ neg_neg _
+
+@[simp] protected theorem neg_mul (u₁ u₂ : units α) : -u₁ * u₂ = -(u₁ * u₂) :=
+units.ext $ neg_mul_eq_neg_mul_symm _ _
+
+@[simp] protected theorem mul_neg (u₁ u₂ : units α) : u₁ * -u₂ = -(u₁ * u₂) :=
+units.ext $ (neg_mul_eq_mul_neg _ _).symm
+
+@[simp] protected theorem neg_mul_neg (u₁ u₂ : units α) : -u₁ * -u₂ = u₁ * u₂ := by simp
+
+protected theorem neg_eq_neg_one_mul (u : units α) : -u = -1 * u := by simp
+
+end units
+
 instance [semiring α] : semiring (with_zero α) :=
 { left_distrib := λ a b c, begin
     cases a with a, {refl},

data/int/basic.lean

@@ -648,6 +648,16 @@ theorem mem_to_nat' : ∀ (a : ℤ) (n : ℕ), n ∈ to_nat' a ↔ a = n
 | (m : ℕ) n := option.some_inj.trans coe_nat_inj'.symm
 | -[1+ m] n := by split; intro h; cases h
 
+/- units -/
+
+@[simp] theorem units_nat_abs (u : units ℤ) : nat_abs u = 1 :=
+units.ext_iff.1 $ nat.units_eq_one ⟨nat_abs u, nat_abs ↑u⁻¹,
+  by rw [← nat_abs_mul, units.mul_inv]; refl,
+  by rw [← nat_abs_mul, units.inv_mul]; refl⟩
+
+theorem units_eq_one_or (u : units ℤ) : u = 1 ∨ u = -1 :=
+by simpa [units.ext_iff, units_nat_abs] using nat_abs_eq u
+
 /- bitwise ops -/
 
 @[simp] lemma bodd_zero : bodd 0 = ff := rfl

ring_theory/localization.lean

@@ -42,32 +42,25 @@ instance : setoid (α × S) :=
 
 def loc := quotient $ localization.setoid α S
 
-private def add_aux : α × S → α × S → loc α S :=
-λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩, ⟦⟨s₁ * r₂ + s₂ * r₁, s₁ * s₂, is_submonoid.mul_mem hs₁ hs₂⟩⟧
-
 instance : has_add (loc α S) :=
-⟨quotient.lift₂ (add_aux α S) $
+⟨quotient.lift₂
+  (λ x y : α × S, (⟦⟨x.2 * y.1 + y.2 * x.1, _, is_submonoid.mul_mem x.2.2 y.2.2⟩⟧ : loc α S)) $
   λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ ⟨r₃, s₃, hs₃⟩ ⟨r₄, s₄, hs₄⟩ ⟨t₅, hts₅, ht₅⟩ ⟨t₆, hts₆, ht₆⟩,
   quotient.sound ⟨t₆ * t₅, is_submonoid.mul_mem hts₆ hts₅,
     calc (s₁ * s₂ * (s₃ * r₄ + s₄ * r₃) - s₃ * s₄ * (s₁ * r₂ + s₂ * r₁)) * (t₆ * t₅) =
       s₁ * s₃ * ((s₂ * r₄ - s₄ * r₂) * t₆) * t₅ + s₂ * s₄ * ((s₁ * r₃ - s₃ * r₁) * t₅) * t₆ : by ring
       ... = 0 : by rw [ht₆, ht₅]; simp⟩⟩
 
-private def neg_aux : α × S → loc α S :=
-λ ⟨r, s, hs⟩, ⟦⟨-r, s, hs⟩⟧
-
 instance : has_neg (loc α S) :=
-⟨quotient.lift (neg_aux α S) $
+⟨quotient.lift (λ x : α × S, (⟦⟨-x.1, x.2⟩⟧ : loc α S)) $
   λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ ⟨t, hts, ht⟩,
   quotient.sound ⟨t, hts,
     calc (s₁ * -r₂ - s₂ * -r₁) * t = -((s₁ * r₂ - s₂ * r₁) * t) : by ring
       ... = 0 : by rw ht; simp⟩⟩
 
-private def mul_aux : α × S → α × S → loc α S :=
-λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩, ⟦⟨r₁ * r₂, s₁ * s₂, is_submonoid.mul_mem hs₁ hs₂⟩⟧
-
 instance : has_mul (loc α S) :=
-⟨quotient.lift₂ (mul_aux α S) $
+⟨quotient.lift₂
+  (λ x y : α × S, (⟦⟨x.1 * y.1, _, is_submonoid.mul_mem x.2.2 y.2.2⟩⟧ : loc α S)) $
   λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ ⟨r₃, s₃, hs₃⟩ ⟨r₄, s₄, hs₄⟩ ⟨t₅, hts₅, ht₅⟩ ⟨t₆, hts₆, ht₆⟩,
   quotient.sound ⟨t₆ * t₅, is_submonoid.mul_mem hts₆ hts₅,
     calc ((s₁ * s₂) * (r₃ * r₄) - (s₃ * s₄) * (r₁ * r₂)) * (t₆ * t₅) =
@@ -201,7 +194,7 @@ lemma mem_non_zero_divisors_of_ne_zero {x : β} :
 
 variable (β)
 
-private def inv_aux : β × (non_zero_divisors β) → quotient_ring β :=
+def inv_aux : β × (non_zero_divisors β) → quotient_ring β :=
 λ ⟨r, s, hs⟩, if h : r = 0 then 0 else ⟦⟨s, r, mem_non_zero_divisors_of_ne_zero h⟩⟧
 
 instance : has_inv (quotient_ring β) :=