michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/algebra/ordered_field): add missing theorems to ordered field

Browse source
This commit is contained in:
Rob Lewis 2015-07-27 23:28:04 -04:00 committed by Rob Lewis
parent 7a4947cfe1
commit c9daf7cbb9
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
library/algebra/ordered_field.lean
View file

@ -266,12 +266,25 @@ section linear_ordered_field
exact mul_lt_mul_of_pos_right H (div_pos_of_pos Hc)
end
theorem div_le_div_of_le_of_pos (H : a ≤ b) (Hc : 0 < c) : a / c ≤ b / c :=
begin
rewrite [{a/c}div_eq_mul_one_div, {b/c}div_eq_mul_one_div],
exact mul_le_mul_of_nonneg_right H (le_of_lt (div_pos_of_pos Hc))
end
theorem div_lt_div_of_lt_of_neg (H : b < a) (Hc : c < 0) : a / c < b / c :=
begin
rewrite [{a/c}div_eq_mul_one_div, {b/c}div_eq_mul_one_div],
exact mul_lt_mul_of_neg_right H (div_neg_of_neg Hc)
end
theorem div_le_div_of_le_of_neg (H : b ≤ a) (Hc : c < 0) : a / c ≤ b / c :=
begin
rewrite [{a/c}div_eq_mul_one_div, {b/c}div_eq_mul_one_div],
exact mul_le_mul_of_nonpos_right H (le_of_lt (div_neg_of_neg Hc))
end
theorem two_ne_zero : (1 : A) + 1 ≠ 0 :=
ne.symm (ne_of_lt (add_pos zero_lt_one zero_lt_one))
@ -312,6 +325,7 @@ theorem nonneg_le_nonneg_of_squares_le (Ha : a ≥ 0) (Hb : b ≥ 0) (H : a * a
a / (1 + 1) < a / (1 + 1) + a / (1 + 1) : lt_add_of_pos_left Ha
... = a : add_halves
end linear_ordered_field
structure discrete_linear_ordered_field [class] (A : Type) extends linear_ordered_field A,