diff --git a/library/algebra/group.lean b/library/algebra/group.lean index 0e267c0e99..9b0b2e9c34 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -251,23 +251,23 @@ section group theorem mul_eq_iff_eq_mul_inv (a b c : A) : a * b = c ↔ a = c * b⁻¹ := iff.intro eq_mul_inv_of_mul_eq mul_eq_of_eq_mul_inv + theorem mul_left_cancel {a b c : A} (H : a * b = a * c) : b = c := + calc b = a⁻¹ * (a * b) : inv_mul_cancel_left + ... = a⁻¹ * (a * c) : H + ... = c : inv_mul_cancel_left + + theorem mul_right_cancel {a b c : A} (H : a * b = c * b) : a = c := + calc a = (a * b) * b⁻¹ : mul_inv_cancel_right + ... = (c * b) * b⁻¹ : H + ... = c : mul_inv_cancel_right + definition group.to_left_cancel_semigroup [instance] [coercion] : left_cancel_semigroup A := ⦃ left_cancel_semigroup, s, - mul_left_cancel := take a b c, - assume H : a * b = a * c, - calc - b = a⁻¹ * (a * b) : inv_mul_cancel_left - ... = a⁻¹ * (a * c) : H - ... = c : inv_mul_cancel_left⦄ + mul_left_cancel := @mul_left_cancel A s ⦄ definition group.to_right_cancel_semigroup [instance] [coercion] : right_cancel_semigroup A := ⦃ right_cancel_semigroup, s, - mul_right_cancel := take a b c, - assume H : a * b = c * b, - calc - a = (a * b) * b⁻¹ : mul_inv_cancel_right - ... = (c * b) * b⁻¹ : H - ... = c : mul_inv_cancel_right⦄ + mul_right_cancel := @mul_right_cancel A s ⦄ end group @@ -378,25 +378,25 @@ section add_group theorem add_eq_iff_eq_add_neg (a b c : A) : a + b = c ↔ a = c + -b := iff.intro eq_add_neg_of_add_eq add_eq_of_eq_add_neg + theorem add_left_cancel {a b c : A} (H : a + b = a + c) : b = c := + calc b = -a + (a + b) : !neg_add_cancel_left⁻¹ + ... = -a + (a + c) : H + ... = c : neg_add_cancel_left + + theorem add_right_cancel {a b c : A} (H : a + b = c + b) : a = c := + calc a = (a + b) + -b : !add_neg_cancel_right⁻¹ + ... = (c + b) + -b : H + ... = c : add_neg_cancel_right + definition add_group.to_left_cancel_semigroup [instance] [coercion] : add_left_cancel_semigroup A := ⦃ add_left_cancel_semigroup, s, - add_left_cancel := take a b c, - assume H : a + b = a + c, - calc - b = -a + (a + b) : !neg_add_cancel_left⁻¹ - ... = -a + (a + c) : H - ... = c : neg_add_cancel_left ⦄ + add_left_cancel := @add_left_cancel A s ⦄ definition add_group.to_add_right_cancel_semigroup [instance] [coercion] : add_right_cancel_semigroup A := ⦃ add_right_cancel_semigroup, s, - add_right_cancel := take a b c, - assume H : a + b = c + b, - calc - a = (a + b) + -b : !add_neg_cancel_right⁻¹ - ... = (c + b) + -b : H - ... = c : add_neg_cancel_right ⦄ + add_right_cancel := @add_right_cancel A s ⦄ /- sub -/ diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index 5bfde7e961..28aa78d62b 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -199,18 +199,16 @@ end structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_pair A := (add_le_add_left : ∀a b, le a b → ∀c, le (add c a) (add c b)) +theorem ordered_comm_group.le_of_add_le_add_left [s : ordered_comm_group A] {a b c : A} (H : a + b ≤ a + c) : b ≤ c := +have H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _, +!neg_add_cancel_left ▸ !neg_add_cancel_left ▸ H' + definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion] [s : ordered_comm_group A] : ordered_cancel_comm_monoid A := ⦃ ordered_cancel_comm_monoid, s, - add_left_cancel := @add.left_cancel _ _, - add_right_cancel := @add.right_cancel _ _, - le_of_add_le_add_left := - proof - take a b c : A, - assume H : a + b ≤ a + c, - have H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _, - !neg_add_cancel_left ▸ !neg_add_cancel_left ▸ H' - qed ⦄ + add_left_cancel := @add.left_cancel A s, + add_right_cancel := @add.right_cancel A s, + le_of_add_le_add_left := @ordered_comm_group.le_of_add_le_add_left A s ⦄ section variables [s : ordered_comm_group A] (a b c d e : A) diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index 1dc61454dd..67f745f784 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -144,51 +144,42 @@ structure ordered_ring [class] (A : Type) extends ring A, ordered_comm_group A : (mul_nonneg : ∀a b, le zero a → le zero b → le zero (mul a b)) (mul_pos : ∀a b, lt zero a → lt zero b → lt zero (mul a b)) +theorem ordered_ring.mul_le_mul_of_nonneg_left [s : ordered_ring A] {a b c : A} + (Hab : a ≤ b) (Hc : 0 ≤ c) : c * a ≤ c * b := +have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab, +have H2 : 0 ≤ c * (b - a), from ordered_ring.mul_nonneg _ _ Hc H1, +iff.mp !sub_nonneg_iff_le (!mul_sub_left_distrib ▸ H2) + +theorem ordered_ring.mul_le_mul_of_nonneg_right [s : ordered_ring A] {a b c : A} + (Hab : a ≤ b) (Hc : 0 ≤ c) : a * c ≤ b * c := +have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab, +have H2 : 0 ≤ (b - a) * c, from ordered_ring.mul_nonneg _ _ H1 Hc, +iff.mp !sub_nonneg_iff_le (!mul_sub_right_distrib ▸ H2) + +theorem ordered_ring.mul_lt_mul_of_pos_left [s : ordered_ring A] {a b c : A} + (Hab : a < b) (Hc : 0 < c) : c * a < c * b := +have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab, +have H2 : 0 < c * (b - a), from ordered_ring.mul_pos _ _ Hc H1, +iff.mp !sub_pos_iff_lt (!mul_sub_left_distrib ▸ H2) + +theorem ordered_ring.mul_lt_mul_of_pos_right [s : ordered_ring A] {a b c : A} + (Hab : a < b) (Hc : 0 < c) : a * c < b * c := +have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab, +have H2 : 0 < (b - a) * c, from ordered_ring.mul_pos _ _ H1 Hc, +iff.mp !sub_pos_iff_lt (!mul_sub_right_distrib ▸ H2) + definition ordered_ring.to_ordered_semiring [instance] [coercion] [s : ordered_ring A] : ordered_semiring A := ⦃ ordered_semiring, s, - mul_zero := mul_zero, - zero_mul := zero_mul, - add_left_cancel := @add.left_cancel A _, - add_right_cancel := @add.right_cancel A _, - le_of_add_le_add_left := @le_of_add_le_add_left A _, - mul_le_mul_of_nonneg_left := take a b c, - assume Hab : a ≤ b, - assume Hc : 0 ≤ c, - show c * a ≤ c * b, - proof - have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab, - have H2 : 0 ≤ c * (b - a), from ordered_ring.mul_nonneg _ _ Hc H1, - iff.mp !sub_nonneg_iff_le (!mul_sub_left_distrib ▸ H2) - qed, - mul_le_mul_of_nonneg_right := take a b c, - assume Hab : a ≤ b, - assume Hc : 0 ≤ c, - show a * c ≤ b * c, - proof - have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab, - have H2 : 0 ≤ (b - a) * c, from ordered_ring.mul_nonneg _ _ H1 Hc, - iff.mp !sub_nonneg_iff_le (!mul_sub_right_distrib ▸ H2) - qed, - mul_lt_mul_of_pos_left := take a b c, - assume Hab : a < b, - assume Hc : 0 < c, - show c * a < c * b, - proof - have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab, - have H2 : 0 < c * (b - a), from ordered_ring.mul_pos _ _ Hc H1, - iff.mp !sub_pos_iff_lt (!mul_sub_left_distrib ▸ H2) - qed, - mul_lt_mul_of_pos_right := take a b c, - assume Hab : a < b, - assume Hc : 0 < c, - show a * c < b * c, - proof - have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab, - have H2 : 0 < (b - a) * c, from ordered_ring.mul_pos _ _ H1 Hc, - iff.mp !sub_pos_iff_lt (!mul_sub_right_distrib ▸ H2) - qed -⦄ + mul_zero := mul_zero, + zero_mul := zero_mul, + add_left_cancel := @add.left_cancel A s, + add_right_cancel := @add.right_cancel A s, + le_of_add_le_add_left := @le_of_add_le_add_left A s, + mul_le_mul_of_nonneg_left := @ordered_ring.mul_le_mul_of_nonneg_left A s, + mul_le_mul_of_nonneg_right := @ordered_ring.mul_le_mul_of_nonneg_right A s, + mul_lt_mul_of_pos_left := @ordered_ring.mul_lt_mul_of_pos_left A s, + mul_lt_mul_of_pos_right := @ordered_ring.mul_lt_mul_of_pos_right A s ⦄ section variable [s : ordered_ring A] @@ -246,39 +237,38 @@ definition linear_ordered_ring.to_linear_ordered_semiring [instance] [coercion] ⦃ linear_ordered_semiring, s, mul_zero := mul_zero, zero_mul := zero_mul, - add_left_cancel := @add.left_cancel A _, - add_right_cancel := @add.right_cancel A _, - le_of_add_le_add_left := @le_of_add_le_add_left A _, - mul_le_mul_of_nonneg_left := @mul_le_mul_of_nonneg_left A _, - mul_le_mul_of_nonneg_right := @mul_le_mul_of_nonneg_right A _, - mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left A _, - mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right A _, - le_total := linear_ordered_ring.le_total -⦄ + add_left_cancel := @add.left_cancel A s, + add_right_cancel := @add.right_cancel A s, + le_of_add_le_add_left := @le_of_add_le_add_left A s, + mul_le_mul_of_nonneg_left := @mul_le_mul_of_nonneg_left A s, + mul_le_mul_of_nonneg_right := @mul_le_mul_of_nonneg_right A s, + mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left A s, + mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right A s, + le_total := linear_ordered_ring.le_total ⦄ structure linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_ring A, comm_monoid A +theorem linear_ordered_comm_ring.eq_zero_or_eq_zero_of_mul_eq_zero [s : linear_ordered_comm_ring A] + {a b : A} (H : a * b = 0) : a = 0 ∨ b = 0 := +lt.by_cases + (assume Ha : 0 < a, + lt.by_cases + (assume Hb : 0 < b, absurd (H ▸ show 0 < a * b, from mul_pos Ha Hb) (lt.irrefl 0)) + (assume Hb : 0 = b, or.inr (Hb⁻¹)) + (assume Hb : 0 > b, absurd (H ▸ show 0 > a * b, from mul_neg_of_pos_of_neg Ha Hb) (lt.irrefl 0))) + (assume Ha : 0 = a, or.inl (Ha⁻¹)) + (assume Ha : 0 > a, + lt.by_cases + (assume Hb : 0 < b, absurd (H ▸ show 0 > a * b, from mul_neg_of_neg_of_pos Ha Hb) (lt.irrefl 0)) + (assume Hb : 0 = b, or.inr (Hb⁻¹)) + (assume Hb : 0 > b, absurd (H ▸ show 0 < a * b, from mul_pos_of_neg_of_neg Ha Hb) (lt.irrefl 0))) + -- Linearity implies no zero divisors. Doesn't need commutativity. definition linear_ordered_comm_ring.to_integral_domain [instance] [coercion] - [s: linear_ordered_comm_ring A] : - integral_domain A := + [s: linear_ordered_comm_ring A] : integral_domain A := ⦃ integral_domain, s, - eq_zero_or_eq_zero_of_mul_eq_zero := take a b, - assume H : a * b = 0, - show a = 0 ∨ b = 0, from - lt.by_cases - (assume Ha : 0 < a, - lt.by_cases - (assume Hb : 0 < b, absurd (H ▸ mul_pos Ha Hb) (lt.irrefl 0)) - (assume Hb : 0 = b, or.inr (Hb⁻¹)) - (assume Hb : 0 > b, absurd (H ▸ mul_neg_of_pos_of_neg Ha Hb) (lt.irrefl 0))) - (assume Ha : 0 = a, or.inl (Ha⁻¹)) - (assume Ha : 0 > a, - lt.by_cases - (assume Hb : 0 < b, absurd (H ▸ mul_neg_of_neg_of_pos Ha Hb) (lt.irrefl 0)) - (assume Hb : 0 = b, or.inr (Hb⁻¹)) - (assume Hb : 0 > b, absurd (H ▸ mul_pos_of_neg_of_neg Ha Hb) (lt.irrefl 0))) -⦄ + eq_zero_or_eq_zero_of_mul_eq_zero := + @linear_ordered_comm_ring.eq_zero_or_eq_zero_of_mul_eq_zero A s ⦄ section variable [s : linear_ordered_ring A] diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 702cb0de62..a6b61a6e6d 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -152,22 +152,24 @@ end comm_semiring structure ring [class] (A : Type) extends add_comm_group A, monoid A, distrib A, zero_ne_one_class A +theorem ring.mul_zero [s : ring A] (a : A) : a * 0 = 0 := +have H : a * 0 + 0 = a * 0 + a * 0, from calc + a * 0 + 0 = a * 0 : add_zero + ... = a * (0 + 0) : {(add_zero 0)⁻¹} + ... = a * 0 + a * 0 : ring.left_distrib, +show a * 0 = 0, from (add.left_cancel H)⁻¹ + +theorem ring.zero_mul [s : ring A] (a : A) : 0 * a = 0 := +have H : 0 * a + 0 = 0 * a + 0 * a, from calc + 0 * a + 0 = 0 * a : add_zero + ... = (0 + 0) * a : {(add_zero 0)⁻¹} + ... = 0 * a + 0 * a : ring.right_distrib, +show 0 * a = 0, from (add.left_cancel H)⁻¹ + definition ring.to_semiring [instance] [coercion] [s : ring A] : semiring A := ⦃ semiring, s, - mul_zero := take a, - have H : a * 0 + 0 = a * 0 + a * 0, from - calc - a * 0 + 0 = a * 0 : add_zero - ... = a * (0 + 0) : {(add_zero 0)⁻¹} - ... = a * 0 + a * 0 : ring.left_distrib, - show a * 0 = 0, from (add.left_cancel H)⁻¹, - zero_mul := take a, - have H : 0 * a + 0 = 0 * a + 0 * a, from - calc - 0 * a + 0 = 0 * a : add_zero - ... = (0 + 0) * a : {(add_zero 0)⁻¹} - ... = 0 * a + 0 * a : ring.right_distrib, - show 0 * a = 0, from (add.left_cancel H)⁻¹ ⦄ + mul_zero := ring.mul_zero, + zero_mul := ring.zero_mul ⦄ section variables [s : ring A] (a b c d e : A)