Commit 2021-01-02 10:18 e35a703f

View on Github →

feat(algebra/ordered_{group,field}): more lemmas relating inv and mul inequalities (#5561) I also renamed inv_le_iff_one_le_mul to inv_le_iff_one_le_mul' for consistency with div_le_iff and div_le_iff' (unprimed lemmas involve multiplication on the right and primed lemmas involve multiplication on the left).

Estimated changes

Modified src/algebra/group_power/lemmas.lean

Modified src/algebra/ordered_field.lean

added theorem inv_pos_le_iff_one_le_mul'

added theorem inv_pos_le_iff_one_le_mul

added theorem inv_pos_lt_iff_one_lt_mul'

added theorem inv_pos_lt_iff_one_lt_mul

Modified src/algebra/ordered_group.lean

added theorem inv_le_iff_one_le_mul'

modified theorem inv_le_iff_one_le_mul

added theorem inv_lt_iff_one_lt_mul'

added theorem inv_lt_iff_one_lt_mul

added theorem le_inv_iff_mul_le_one'

added theorem lt_inv_iff_mul_lt_one'

added theorem lt_inv_iff_mul_lt_one

Modified src/analysis/convex/cone.lean