max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/algebra/ordered_field): remove unused argument from div_two_lt_of_pos

Browse source
This commit is contained in:
Johannes Hölzl 2017-08-23 16:13:28 -04:00 • committed by Gabriel Ebner
parent 3062c6feb7
commit 2e5284add7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/algebra/ordered_field.lean
View file

@ -319,7 +319,7 @@ begin
apply le_mul_of_div_le hc h
end
lemma div_two_lt_of_pos {a b : α} (h : a > 0) : a / 2 < a :=
lemma div_two_lt_of_pos {a : α} (h : a > 0) : a / 2 < a :=
suffices a / (1 + 1) < a, begin unfold bit0, assumption end,
have ha : a / 2 > 0, from div_pos_of_pos_of_pos h (add_pos zero_lt_one zero_lt_one),
calc