Commit 2020-08-15 20:41 d40c06f0

feat(algebra/ordered_field): rewrite and cleanup (#3751) Group similar lemmas in a more intuitive way Add docstrings, module doc and section headers Simplify some proofs Remove some implications if they had a corresponding iff lemma. Add some more variants of some lemmas Rename some lemmas for consistency List of name changes (the lemma on the right might be a bi-implication, if the original version was an implication): add_midpoint -> add_sub_div_two_lt le_div_of_mul_le, mul_le_of_le_div -> le_div_iff lt_div_of_mul_lt, mul_lt_of_lt_div -> lt_div_iff div_le_of_le_mul -> div_le_iff' le_mul_of_div_le -> div_le_iff div_lt_of_pos_of_lt_mul -> div_lt_iff' mul_le_of_neg_of_div_le, div_le_of_neg_of_mul_le -> div_le_iff_of_neg mul_lt_of_neg_of_div_lt, div_lt_of_neg_of_mul_lt -> div_lt_iff_of_neg div_le_div_of_pos_of_le -> div_le_div_of_le div_le_div_of_neg_of_le -> div_le_div_of_nonpos_of_le div_lt_div_of_pos_of_lt -> div_lt_div_of_lt div_mul_le_div_mul_of_div_le_div_nonneg -> div_mul_le_div_mul_of_div_le_div one_le_div_of_le, le_of_one_le_div, one_le_div_iff_le -> one_le_div one_lt_div_of_lt, lt_of_one_lt_div, one_lt_div_iff_lt -> one_lt_div div_le_one_iff_le -> div_le_one div_lt_one_iff_lt -> div_lt_one one_div_le_of_pos_of_one_div_le -> one_div_le one_div_le_of_neg_of_one_div_le -> one_div_le_of_neg div_lt_div_of_pos_of_lt_of_pos -> div_lt_div_of_lt_left One regression I noticed in some other files: when using div_le_iff, and the argument is proven by some lemma about linear_ordered_semiring then Lean gives a type mismatch. Presumably this happens because the instance chain ordered_field -> has_le doesn't go via ordered_semiring. The fix is to give the type explicitly, for example using div_le_iff (t : (0 : ℝ) < _)