diff --git a/library/algebra/field.lean b/library/algebra/field.lean index ae8e3ccbf..878ed0787 100644 --- a/library/algebra/field.lean +++ b/library/algebra/field.lean @@ -17,7 +17,7 @@ namespace algebra variable {A : Type} -structure division_ring [class] (A : Type) extends ring A, has_inv A := +structure division_ring [class] (A : Type) extends ring A, has_inv A, zero_ne_one_class A := (mul_inv_cancel : ∀{a}, a ≠ zero → mul a (inv a) = one) (inv_mul_cancel : ∀{a}, a ≠ zero → mul (inv a) a = one) @@ -40,21 +40,21 @@ section division_ring theorem inv_eq_one_div : a⁻¹ = 1 / a := !one_mul⁻¹ theorem div_eq_mul_one_div : a / b = a * (1 / b) := - by rewrite [↑divide, one_mul] + by rewrite [↑divide, one_mul] theorem mul_one_div_cancel (H : a ≠ 0) : a * (1 / a) = 1 := by rewrite [-inv_eq_one_div, (mul_inv_cancel H)] theorem one_div_mul_cancel (H : a ≠ 0) : (1 / a) * a = 1 := by rewrite [-inv_eq_one_div, (inv_mul_cancel H)] - + theorem div_self (H : a ≠ 0) : a / a = 1 := mul_inv_cancel H theorem mul_div_assoc : (a * b) / c = a * (b / c) := !mul.assoc theorem one_div_ne_zero (H : a ≠ 0) : 1 / a ≠ 0 := assume H2 : 1 / a = 0, - have C1 : 0 = 1, from symm (by rewrite [-(mul_one_div_cancel H), H2, mul_zero]), + have C1 : 0 = 1, from symm (by rewrite [-(mul_one_div_cancel H), H2, mul_zero]), absurd C1 zero_ne_one -- the analogue in group is called inv_one @@ -93,7 +93,7 @@ section division_ring -- make "left" and "right" versions? theorem eq_one_div_of_mul_eq_one (H : a * b = 1) : b = 1 / a := - have H2 : a ≠ 0, from + have H2 : a ≠ 0, from (assume A : a = 0, have B : 0 = 1, by rewrite [-(zero_mul b), -A, H], absurd B zero_ne_one), @@ -106,7 +106,7 @@ section division_ring -- which one is left and which is right? theorem eq_one_div_of_mul_eq_one_left (H : b * a = 1) : b = 1 / a := - have H2 : a ≠ 0, from + have H2 : a ≠ 0, from (assume A : a = 0, have B : 0 = 1, from symm (calc 1 = b * a : symm H @@ -121,9 +121,9 @@ section division_ring ... = b : mul_one) theorem one_div_mul_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) : (1 / a) * (1 / b) = 1 / (b * a) := - have H : (b * a) * ((1 / a) * (1 / b)) = 1, by + have H : (b * a) * ((1 / a) * (1 / b)) = 1, by rewrite [mul.assoc, -(mul.assoc a), (mul_one_div_cancel Ha), one_mul, (mul_one_div_cancel Hb)], - eq_one_div_of_mul_eq_one H + eq_one_div_of_mul_eq_one H theorem one_div_neg_one_eq_neg_one : 1 / (-1) = -1 := have H : (-1) * (-1) = 1, by rewrite [-neg_eq_neg_one_mul, neg_neg], @@ -135,10 +135,10 @@ section division_ring a + a * -1 = a * 1 + a * -1 : mul_one ... = a * (1 + -1) : left_distrib ... = a * 0 : add.right_inv - ... = 0 : mul_zero, + ... = 0 : mul_zero, symm (neg_eq_of_add_eq_zero H) - theorem one_div_neg_eq_neg_one_div (H : a ≠ 0) : 1 / (- a) = - (1 / a) := + theorem one_div_neg_eq_neg_one_div (H : a ≠ 0) : 1 / (- a) = - (1 / a) := have H1 : -1 ≠ 0, from (assume H2 : -1 = 0, absurd (symm (calc 1 = -(-1) : neg_neg @@ -146,7 +146,7 @@ section division_ring ... = 0 : neg_zero)) zero_ne_one), calc 1 / (- a) = 1 / ((-1) * a) : neg_eq_neg_one_mul - ... = (1 / a) * (1 / (- 1)) : one_div_mul_one_div H H1 + ... = (1 / a) * (1 / (- 1)) : one_div_mul_one_div H H1 ... = (1 / a) * (-1) : one_div_neg_one_eq_neg_one ... = - (1 / a) : mul_neg_one_eq_neg @@ -184,7 +184,7 @@ section division_ring theorem div_mul_cancel (Hb : b ≠ 0) : a / b * b = a := by rewrite [↑divide, mul.assoc, (inv_mul_cancel Hb), mul_one] - + theorem div_add_div_same : a / c + b / c = (a + b) / c := !right_distrib⁻¹ theorem inv_mul_add_mul_inv_eq_inv_add_inv (Ha : a ≠ 0) (Hb : b ≠ 0) : @@ -197,7 +197,7 @@ section division_ring by rewrite [(mul_sub_left_distrib (1 / a)), (one_div_mul_cancel Ha), mul_sub_right_distrib, one_mul, mul.assoc, (mul_one_div_cancel Hb), mul_one, one_mul] - theorem div_eq_one_iff_eq (Hb : b ≠ 0) : a / b = 1 ↔ a = b := + theorem div_eq_one_iff_eq (Hb : b ≠ 0) : a / b = 1 ↔ a = b := iff.intro (assume H1 : a / b = 1, symm (calc b = 1 * b : one_mul @@ -268,10 +268,10 @@ section field theorem div_mul_eq_mul_div (Hc : c ≠ 0) : (b / c) * a = (b * a) / c := by rewrite [↑divide, mul.assoc, (mul.comm c⁻¹), -mul.assoc] - + -- this one is odd -- I am not sure what to call it, but again, the prefix is right theorem div_mul_eq_mul_div_comm (Hc : c ≠ 0) : (b / c) * a = b * (a / c) := - by rewrite [(div_mul_eq_mul_div Hc), -(one_mul c), -(div_mul_div (ne.symm zero_ne_one) Hc), div_one, one_mul] + by rewrite [(div_mul_eq_mul_div Hc), -(one_mul c), -(div_mul_div (ne.symm zero_ne_one) Hc), div_one, one_mul] theorem div_add_div (Hb : b ≠ 0) (Hd : d ≠ 0) : (a / b) + (c / d) = ((a * d) + (b * c)) / (b * d) := @@ -282,7 +282,7 @@ section field (a / b) - (c / d) = ((a * d) - (b * c)) / (b * d) := by rewrite [↑sub, neg_eq_neg_one_mul, -mul_div_assoc, (div_add_div Hb Hd), -mul.assoc, (mul.comm b), mul.assoc, -neg_eq_neg_one_mul] - + theorem mul_eq_mul_of_div_eq_div (Hb : b ≠ 0) (Hd : d ≠ 0) (H : a / b = c / d) : a * d = c * b := by rewrite [-mul_one, mul.assoc, (mul.comm d), -mul.assoc, -(div_self Hb), -(div_mul_eq_mul_div_comm Hb), H, (div_mul_eq_mul_div Hd), (div_mul_cancel Hd)] @@ -323,9 +323,9 @@ section discrete_field decidable.by_cases (assume H : x = 0, or.inl H) (assume H1 : x ≠ 0, - or.inr (by rewrite [-one_mul, -(inv_mul_cancel H1), mul.assoc, H, mul_zero])) + or.inr (by rewrite [-one_mul, -(inv_mul_cancel H1), mul.assoc, H, mul_zero])) - definition discrete_field.to_integral_domain [instance] [reducible] [coercion] : + definition discrete_field.to_integral_domain [instance] [reducible] [coercion] : integral_domain A := ⦃ integral_domain, s, eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero⦄ diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index 86a6a7059..5009690a0 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -22,7 +22,7 @@ absurd H (lt.irrefl a) structure ordered_semiring [class] (A : Type) extends has_mul A, has_zero A, has_lt A, -- TODO: remove hack for improving performance - semiring A, ordered_cancel_comm_monoid A := + semiring A, ordered_cancel_comm_monoid A, zero_ne_one_class A := (mul_le_mul_of_nonneg_left: ∀a b c, le a b → le zero c → le (mul c a) (mul c b)) (mul_le_mul_of_nonneg_right: ∀a b c, le a b → le zero c → le (mul a c) (mul b c)) (mul_lt_mul_of_pos_left: ∀a b c, lt a b → lt zero c → lt (mul c a) (mul c b)) @@ -147,7 +147,7 @@ section not_lt_of_le H3 H) end -structure ordered_ring [class] (A : Type) extends ring A, ordered_comm_group A := +structure ordered_ring [class] (A : Type) extends ring A, ordered_comm_group A, zero_ne_one_class 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)) diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 3addd257f..5ae8ef411 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -44,7 +44,7 @@ theorem zero_ne_one [s: zero_ne_one_class A] : 0 ≠ 1 := @zero_ne_one_class.zer /- semiring -/ structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A, distrib A, - mul_zero_class A, zero_ne_one_class A + mul_zero_class A section semiring variables [s : semiring A] (a b c : A) @@ -148,7 +148,7 @@ end comm_semiring /- ring -/ -structure ring [class] (A : Type) extends add_comm_group A, monoid A, distrib A, zero_ne_one_class A +structure ring [class] (A : Type) extends add_comm_group A, monoid A, distrib A theorem ring.mul_zero [s : ring A] (a : A) : a * 0 = 0 := have H : a * 0 + 0 = a * 0 + a * 0, from calc diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 93cf9ee4e..9c4db64f1 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -629,7 +629,6 @@ section mul_one := mul_one, left_distrib := mul.left_distrib, right_distrib := mul.right_distrib, - zero_ne_one := zero_ne_one, mul_comm := mul.comm, eq_zero_or_eq_zero_of_mul_eq_zero := @eq_zero_or_eq_zero_of_mul_eq_zero⦄ end diff --git a/library/data/int/order.lean b/library/data/int/order.lean index d3cb9a397..e7e09947d 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -233,7 +233,8 @@ section mul_nonneg := @mul_nonneg, mul_pos := @mul_pos, le_iff_lt_or_eq := le_iff_lt_or_eq, - le_total := le.total⦄ + le_total := le.total, + zero_ne_one := zero_ne_one⦄ protected definition decidable_linear_ordered_comm_ring [instance] [reducible] : algebra.decidable_linear_ordered_comm_ring int := diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 7f6a604aa..1b0d87039 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -307,7 +307,6 @@ section right_distrib := mul.right_distrib, zero_mul := zero_mul, mul_zero := mul_zero, - zero_ne_one := ne.symm (succ_ne_zero zero), mul_comm := mul.comm⦄ end diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 6bc56c801..115955741 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -161,6 +161,7 @@ section lt_iff_le_ne := lt_iff_le_and_ne, add_le_add_left := @add_le_add_left, le_of_add_le_add_left := @le_of_add_le_add_left, + zero_ne_one := ne.symm (succ_ne_zero zero), mul_le_mul_of_nonneg_left := (take a b c H1 H2, mul_le_mul_left H1 c), mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right H1 c), mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left,