feat(algebra): new algebra theorems (more iff)

algebra/big_operators.lean

@@ -161,9 +161,7 @@ end finset
 run_cmd transport_multiplicative_to_additive [
   /- map operations -/
   (`has_mul.mul, `has_add.add), (`has_one.one, `has_zero.zero), (`has_inv.inv, `has_neg.neg),
-  (`has_mul, `has_add), (`has_one, `has_zero), (`has_inv, `has_neg),
-  /- map constructors -/
-  (`has_mul.mk, `has_add.mk), (`has_one, `has_zero.mk), (`has_inv, `has_neg.mk),
+  (`has_one, `has_zero), (`has_mul, `has_add), (`has_inv, `has_neg),
   /- map structures -/
   (`semigroup, `add_semigroup),
   (`monoid, `add_monoid),
@@ -190,16 +188,6 @@ run_cmd transport_multiplicative_to_additive [
   (`comm_group.to_comm_monoid, `add_comm_group.to_add_comm_monoid),
   (`left_cancel_semigroup.to_semigroup, `add_left_cancel_semigroup.to_add_semigroup),
   (`right_cancel_semigroup.to_semigroup, `add_right_cancel_semigroup.to_add_semigroup),
-  /- map projections -/
-  (`semigroup.mul_assoc, `add_semigroup.add_assoc),
-  (`comm_semigroup.mul_comm, `add_comm_semigroup.add_comm),
-  (`left_cancel_semigroup.mul_left_cancel, `add_left_cancel_semigroup.add_left_cancel),
-  (`right_cancel_semigroup.mul_right_cancel, `add_right_cancel_semigroup.add_right_cancel),
-  (`monoid.one_mul, `add_monoid.zero_add),
-  (`monoid.mul_one, `add_monoid.add_zero),
-  (`group.mul_left_inv, `add_group.add_left_neg),
-  (`group.mul, `add_group.add),
-  (`group.mul_assoc, `add_group.add_assoc),
   /- map lemmas -/
   (`mul_assoc, `add_assoc),
   (`mul_comm, `add_comm),
@@ -210,45 +198,16 @@ run_cmd transport_multiplicative_to_additive [
   (`mul_left_inv, `add_left_neg),
   (`mul_left_cancel, `add_left_cancel),
   (`mul_right_cancel, `add_right_cancel),
-  (`mul_left_cancel_iff, `add_left_cancel_iff),
-  (`mul_right_cancel_iff, `add_right_cancel_iff),
   (`inv_mul_cancel_left, `neg_add_cancel_left),
   (`inv_mul_cancel_right, `neg_add_cancel_right),
-  (`eq_inv_mul_of_mul_eq, `eq_neg_add_of_add_eq),
-  (`inv_eq_of_mul_eq_one, `neg_eq_of_add_eq_zero),
   (`inv_inv, `neg_neg),
-  (`mul_right_inv, `add_right_neg),
   (`mul_inv_cancel_left, `add_neg_cancel_left),
   (`mul_inv_cancel_right, `add_neg_cancel_right),
-  (`mul_inv_rev, `neg_add_rev),
   (`mul_inv, `neg_add),
-  (`inv_inj, `neg_inj),
-  (`group.mul_left_cancel, `add_group.add_left_cancel),
-  (`group.mul_right_cancel, `add_group.add_right_cancel),
-  (`group.to_left_cancel_semigroup, `add_group.to_left_cancel_add_semigroup),
   (`group.to_right_cancel_semigroup, `add_group.to_right_cancel_add_semigroup),
   (`eq_inv_of_eq_inv, `eq_neg_of_eq_neg),
-  (`eq_inv_of_mul_eq_one, `eq_neg_of_add_eq_zero),
-  (`eq_mul_inv_of_mul_eq, `eq_add_neg_of_add_eq),
-  (`inv_mul_eq_of_eq_mul, `neg_add_eq_of_eq_add),
-  (`mul_inv_eq_of_eq_mul, `add_neg_eq_of_eq_add),
-  (`eq_mul_of_mul_inv_eq, `eq_add_of_add_neg_eq),
-  (`eq_mul_of_inv_mul_eq, `eq_add_of_neg_add_eq),
-  (`mul_eq_of_eq_inv_mul, `add_eq_of_eq_neg_add),
-  (`mul_eq_of_eq_mul_inv, `add_eq_of_eq_add_neg),
   (`one_inv, `neg_zero),
-  (`left_inverse_inv, `left_inverse_neg),
-  (`inv_eq_inv_iff_eq, `neg_eq_neg_iff_eq),
-  (`inv_eq_one_iff_eq_one, `neg_eq_zero_iff_eq_zero),
-  (`eq_one_of_inv_eq_one, `eq_zero_of_neg_eq_zero),
-  (`eq_inv_iff_eq_inv, `eq_neg_iff_eq_neg),
-  (`eq_of_mul_inv_eq_one, `eq_of_add_neg_eq_zero),
-  (`mul_eq_iff_eq_inv_mul, `add_eq_iff_eq_neg_add),
-  (`mul_eq_iff_eq_mul_inv, `add_eq_iff_eq_add_neg),
-  -- (`mul_eq_one_of_mul_eq_one, `add_eq_zero_of_add_eq_zero)   not needed for commutative groups
-  -- (`muleq_one_iff_mul_eq_one, `add_eq_zero_iff_add_eq_zero)
-
-  --NEW:
+  /- new lemmas -/
   (`list.prod, `list.sum),
   (`list.prod.equations._eqn_1, `list.sum.equations._eqn_1),
   (`list.prod_nil, `list.sum_nil),

algebra/functions.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+
+universe u
+variables {α : Type u}
+
+section
+variables [decidable_linear_order α] {a b c : α}
+
+lemma le_min_iff : c ≤ min a b ↔ c ≤ a ∧ c ≤ b :=
+⟨λ h, ⟨le_trans h (min_le_left a b), le_trans h (min_le_right a b)⟩,
+ λ ⟨h₁, h₂⟩, le_min h₁ h₂⟩
+
+lemma max_le_iff : max a b ≤ c ↔ a ≤ c ∧ b ≤ c :=
+⟨λ h, ⟨le_trans (le_max_left a b) h, le_trans (le_max_right a b) h⟩,
+ λ ⟨h₁, h₂⟩, max_le h₁ h₂⟩
+
+end
+
+section decidable_linear_ordered_comm_group
+variables [decidable_linear_ordered_comm_group α] {a b : α}
+
+theorem abs_le : abs a ≤ b ↔ (- b ≤ a ∧ a ≤ b) :=
+⟨assume h, ⟨neg_le_of_neg_le $ le_trans (neg_le_abs_self _) h, le_trans (le_abs_self _) h⟩,
+  assume ⟨h₁, h₂⟩, abs_le_of_le_of_neg_le h₂ $ neg_le_of_neg_le h₁⟩
+
+lemma abs_lt : abs a < b ↔ (- b < a ∧ a < b) :=
+⟨assume h, ⟨neg_lt_of_neg_lt $ lt_of_le_of_lt (neg_le_abs_self _) h, lt_of_le_of_lt (le_abs_self _) h⟩,
+  assume ⟨h₁, h₂⟩, abs_lt_of_lt_of_neg_lt h₂ $ neg_lt_of_neg_lt h₁⟩
+
+@[simp] lemma abs_eq_zero : abs a = 0 ↔ a = 0 :=
+⟨eq_zero_of_abs_eq_zero, λ e, e.symm ▸ abs_zero⟩
+
+end decidable_linear_ordered_comm_group