From 00262e4e47c27b7b58a2ed632c745399f7218ee7 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Wed, 5 Aug 2015 17:03:46 -0400 Subject: [PATCH] feat(library/algebra): finish adding one-directional versions of iff theorems --- library/algebra/field.lean | 9 +++++++++ library/algebra/ordered_field.lean | 15 ++++++--------- library/algebra/ordered_ring.lean | 6 ++++++ library/algebra/ring.lean | 20 +++++++++++++++++++- 4 files changed, 40 insertions(+), 10 deletions(-) diff --git a/library/algebra/field.lean b/library/algebra/field.lean index de649d151..8b457ab14 100644 --- a/library/algebra/field.lean +++ b/library/algebra/field.lean @@ -200,11 +200,20 @@ section division_ring a / b = b / b : this ... = 1 : div_self Hb) + theorem eq_of_div_eq_one (Hb : b ≠ 0) : a / b = 1 → a = b := + iff.mp (div_eq_one_iff_eq Hb) + theorem eq_div_iff_mul_eq (Hc : c ≠ 0) : a = b / c ↔ a * c = b := iff.intro (suppose a = b / c, by rewrite [this, (div_mul_cancel Hc)]) (suppose a * c = b, by rewrite [-(mul_div_cancel Hc), this]) + theorem eq_div_of_mul_eq (Hc : c ≠ 0) : a * c = b → a = b / c := + iff.mpr (eq_div_iff_mul_eq Hc) + + theorem mul_eq_of_eq_div (Hc : c ≠ 0) : a = b / c → a * c = b := + iff.mp (eq_div_iff_mul_eq Hc) + theorem add_div_eq_mul_add_div (Hc : c ≠ 0) : a + b / c = (a * c + b) / c := have (a + b / c) * c = a * c + b, by rewrite [right_distrib, (div_mul_cancel Hc)], (iff.elim_right (eq_div_iff_mul_eq Hc)) this diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index 756f5afef..8c0d866eb 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -399,7 +399,6 @@ section discrete_linear_ordered_field have H3 : 0 < -a, from pos_of_div_pos H2, neg_of_neg_pos H3 --- why is mul_le_mul under ordered_ring namespace? theorem le_of_div_le (H : 0 < a) (Hl : 1 / a ≤ 1 / b) : b ≤ a := have Hb : 0 < b, from pos_of_div_pos (calc 0 < 1 / a : div_pos_of_pos H @@ -407,11 +406,10 @@ section discrete_linear_ordered_field have H' : 1 ≤ a / b, from (calc 1 = a / a : div_self (ne.symm (ne_of_lt H)) ... = a * (1 / a) : div_eq_mul_one_div - ... ≤ a * (1 / b) : ordered_ring.mul_le_mul_of_nonneg_left Hl (le_of_lt H) + ... ≤ a * (1 / b) : mul_le_mul_of_nonneg_left Hl (le_of_lt H) ... = a / b : div_eq_mul_one_div ), le_of_one_le_div Hb H' - theorem le_of_div_le_neg (H : b < 0) (Hl : 1 / a ≤ 1 / b) : b ≤ a := assert Ha : a ≠ 0, from ne_of_lt (neg_of_div_neg (calc 1 / a ≤ 1 / b : Hl @@ -480,14 +478,13 @@ section discrete_linear_ordered_field theorem div_lt_div_of_pos_of_lt_of_pos (Hb : 0 < b) (H : b < a) (Hc : 0 < c) : c / a < c / b := begin - apply iff.mp (sub_neg_iff_lt _ _), - rewrite [div_eq_mul_one_div, {c / b}div_eq_mul_one_div], - rewrite -mul_sub_left_distrib, + apply iff.mp !sub_neg_iff_lt, + rewrite [div_eq_mul_one_div, {c / b}div_eq_mul_one_div, -mul_sub_left_distrib], apply mul_neg_of_pos_of_neg, exact Hc, - apply iff.mpr (sub_neg_iff_lt _ _), + apply iff.mpr !sub_neg_iff_lt, apply div_lt_div_of_lt, - exact Hb, exact H + repeat assumption end theorem div_mul_le_div_mul_of_div_le_div_pos' {d e : A} (H : a / b ≤ c / d) @@ -507,7 +504,7 @@ section discrete_linear_ordered_field by rewrite [abs_of_neg H', abs_of_neg (div_neg_of_neg H'), -(one_div_neg_eq_neg_one_div (ne_of_lt H'))] else - have Heq [visible] : a = 0, from eq_of_le_of_ge (le_of_not_gt H) (le_of_not_gt H'), + assert Heq : a = 0, from eq_of_le_of_ge (le_of_not_gt H) (le_of_not_gt H'), by rewrite [Heq, div_zero, *abs_zero, div_zero]) theorem ge_sub_of_abs_sub_le_left (H : abs (a - b) ≤ c) : a ≥ b - c := diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index 037566b91..cc4eb2e8a 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -603,9 +603,15 @@ section theorem abs_dvd_iff (a b : A) : abs a ∣ b ↔ a ∣ b := abs.by_cases !iff.refl !neg_dvd_iff_dvd + theorem abs_dvd_of_dvd {a b : A} : a ∣ b → abs a ∣ b := + iff.mpr !abs_dvd_iff + theorem dvd_abs_iff (a b : A) : a ∣ abs b ↔ a ∣ b := abs.by_cases !iff.refl !dvd_neg_iff_dvd + theorem dvd_abs_of_dvd {a b : A} : a ∣ b → a ∣ abs b := + iff.mpr !dvd_abs_iff + theorem abs_mul (a b : A) : abs (a * b) = abs a * abs b := or.elim (le.total 0 a) (assume H1 : 0 ≤ a, diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 87a1c9d6b..aa2d29e56 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -222,6 +222,12 @@ section ... ↔ a * e - b * e + c = d : by rewrite sub_add_eq_add_sub ... ↔ (a - b) * e + c = d : by rewrite mul_sub_right_distrib + theorem mul_add_eq_mul_add_of_sub_mul_add_eq : (a - b) * e + c = d → a * e + c = b * e + d := + iff.mpr !mul_add_eq_mul_add_iff_sub_mul_add_eq + + theorem sub_mul_add_eq_of_mul_add_eq_mul_add : a * e + c = b * e + d → (a - b) * e + c = d := + iff.mp !mul_add_eq_mul_add_iff_sub_mul_add_eq + theorem mul_neg_one_eq_neg : a * (-1) = -a := have a + a * -1 = 0, from calc a + a * -1 = a * 1 + a * -1 : mul_one @@ -278,6 +284,12 @@ section (show a * -c = -b, by rewrite [-neg_mul_eq_mul_neg, -this]))) + theorem dvd_neg_of_dvd : (a ∣ b) → (a ∣ -b) := + iff.mpr !dvd_neg_iff_dvd + + theorem dvd_of_dvd_neg : (a ∣ -b) → (a ∣ b) := + iff.mp !dvd_neg_iff_dvd + theorem neg_dvd_iff_dvd : (-a ∣ b) ↔ (a ∣ b) := iff.intro (suppose -a ∣ b, @@ -291,8 +303,14 @@ section dvd.intro (show -a * -c = b, by rewrite [neg_mul_neg, this]))) + theorem neg_dvd_of_dvd : (a ∣ b) → (-a ∣ b) := + iff.mpr !neg_dvd_iff_dvd + + theorem dvd_of_neg_dvd : (-a ∣ b) → (a ∣ b) := + iff.mp !neg_dvd_iff_dvd + theorem dvd_sub (H₁ : (a ∣ b)) (H₂ : (a ∣ c)) : (a ∣ b - c) := - dvd_add H₁ (iff.elim_right !dvd_neg_iff_dvd H₂) + dvd_add H₁ (!dvd_neg_of_dvd H₂) end /- integral domains -/