| Metric | Count |
|---|
DefinitionsAddLECancellable, toAddLeftCancelSemigroup, toAddRightCancelSemigroup, toLeftCancelSemigroup, toRightCancelSemigroup, MulLECancellable | 6 |
Theoremsadd, add_le_add_iff_left, add_le_add_iff_right, add_le_iff_nonpos_left, add_le_iff_nonpos_right, inj, inj_left, injective_left, isAddLeftRegular, le_add_iff_nonneg_left, le_add_iff_nonneg_right, of_add_left, of_add_right, toIsLeftCancelAdd, toIsRightCancelAdd, add, add_const, add_strictAnti, const_add, const_mul', mul', mul_const', mul_strictAnti', add, add_const, add_strictAnti, const_add, const_mul', mul', mul_const', mul_strictAnti', AddLECancellable, MulLECancellable, instAddLeftMono, add_lt_add, add_neg, add_neg', add_neg_of_neg_of_nonpos, add_neg_of_nonpos_of_neg, add_nonneg, add_nonpos, add_pos, add_pos', add_pos_of_nonneg_of_pos, add_pos_of_pos_of_nonneg, min_le_max_of_add_le_add, min_le_max_of_mul_le_mul, mul_le_one, mul_lt_mul, mul_lt_one, mul_lt_one', mul_lt_one_of_le_of_lt, mul_lt_one_of_lt_of_le, one_le_mul, one_lt_mul, one_lt_mul', one_lt_mul_of_le_of_lt, one_lt_mul_of_lt_of_le, add, add_const, add_strictMono, const_add, const_mul', mul', mul_const', mul_strictMono', add, add_const, add_strictMono, const_add, const_mul', mul', mul_const', mul_strictMono', inj, inj_left, injective_left, isLeftRegular, le_mul_iff_one_le_left, le_mul_iff_one_le_right, mul, mul_le_iff_le_one_left, mul_le_iff_le_one_right, mul_le_mul_iff_left, mul_le_mul_iff_right, of_mul_left, of_mul_right, toIsLeftCancelMul, toIsRightCancelMul, instMulLeftMono, add_lt_add, add_neg, add_neg', add_neg_of_neg_of_nonpos, add_neg_of_nonpos_of_neg, add_nonneg, add_nonpos, add_pos, add_pos', add_pos_of_nonneg_of_pos, add_pos_of_pos_of_nonneg, min_le_max_of_add_le_add, min_le_max_of_mul_le_mul, mul_le_one, mul_lt_mul, mul_lt_one, mul_lt_one', mul_lt_one_of_le_of_lt, mul_lt_one_of_lt_of_le, one_le_mul, one_lt_mul, one_lt_mul', one_lt_mul_of_le_of_lt, one_lt_mul_of_lt_of_le, add, add_antitone, add_const, const_add, const_mul', mul', mul_antitone', mul_const', add, add_antitone, add_const, const_add, const_mul', mul', mul_antitone', mul_const', add, add_const, add_monotone, const_add, const_mul', mul', mul_const', mul_monotone', add, add_const, add_monotone, const_add, const_mul', mul', mul_const', mul_monotone', addLECancellable_add, addLECancellable_zero, add_eq_add_iff_eq_and_eq, add_eq_zero_iff_of_nonneg, add_le_add, add_le_add_iff_left, add_le_add_iff_of_ge, add_le_add_iff_right, add_le_add_left, add_le_add_right, add_le_add_three, add_le_iff_nonpos_left, add_le_iff_nonpos_right, add_le_of_add_le_left, add_le_of_add_le_right, add_le_of_le_of_nonpos, add_le_of_nonpos_left, add_le_of_nonpos_of_le, add_le_of_nonpos_right, add_left_cancel'', add_left_inj_of_comparable, add_left_mono, add_left_strictMono, add_lt_add, add_lt_add_iff_left, add_lt_add_iff_right, add_lt_add_left, add_lt_add_of_le_of_lt, add_lt_add_of_lt_of_le, add_lt_add_of_lt_of_lt, add_lt_add_right, add_lt_iff_neg_left, add_lt_iff_neg_right, add_lt_of_add_lt_left, add_lt_of_add_lt_right, add_lt_of_le_of_neg, add_lt_of_lt_of_neg, add_lt_of_lt_of_neg', add_lt_of_lt_of_nonpos, add_lt_of_neg_left, add_lt_of_neg_of_le, add_lt_of_neg_of_lt, add_lt_of_neg_of_lt', add_lt_of_neg_right, add_lt_of_nonpos_of_lt, add_max, add_min, add_neg, add_neg', add_neg_of_neg_of_nonpos, add_neg_of_nonpos_of_neg, add_nonneg, add_nonpos, add_pos, add_pos', add_pos_of_nonneg_of_pos, add_pos_of_pos_of_nonneg, add_right_cancel'', add_right_inj_of_comparable, add_right_mono, add_right_strictMono, cmp_add_left, cmp_add_right, cmp_mul_left', cmp_mul_right', eq_one_of_mul_le_one_left, eq_one_of_mul_le_one_right, eq_one_of_one_le_mul_left, eq_one_of_one_le_mul_right, eq_zero_of_add_nonneg_left, eq_zero_of_add_nonneg_right, eq_zero_of_add_nonpos_left, eq_zero_of_add_nonpos_right, exists_square_le, instIsLeftCancelAddOfAddLeftReflectLE, instIsLeftCancelMulOfMulLeftReflectLE, instIsRightCancelAddOfAddRightReflectLE, instIsRightCancelMulOfMulRightReflectLE, le_add_iff_nonneg_left, le_add_iff_nonneg_right, le_add_of_le_add_left, le_add_of_le_add_right, le_add_of_le_of_nonneg, le_add_of_nonneg_left, le_add_of_nonneg_of_le, le_add_of_nonneg_right, le_mul_iff_one_le_left', le_mul_iff_one_le_right', le_mul_of_le_mul_left, le_mul_of_le_mul_right, le_mul_of_le_of_one_le, le_mul_of_one_le_left', le_mul_of_one_le_of_le, le_mul_of_one_le_right', le_of_add_le_add_left, le_of_add_le_add_right, le_of_add_le_of_nonneg_left, le_of_add_le_of_nonneg_right, le_of_le_add_of_nonpos_left, le_of_le_add_of_nonpos_right, le_of_le_mul_of_le_one_left, le_of_le_mul_of_le_one_right, le_of_mul_le_mul_left', le_of_mul_le_mul_right', le_of_mul_le_of_one_le_left, le_of_mul_le_of_one_le_right, le_one_of_mul_le_left, le_one_of_mul_le_right, lt_add_iff_pos_left, lt_add_iff_pos_right, lt_add_of_le_of_pos, lt_add_of_lt_add_left, lt_add_of_lt_add_right, lt_add_of_lt_of_nonneg, lt_add_of_lt_of_pos, lt_add_of_lt_of_pos', lt_add_of_nonneg_of_lt, lt_add_of_pos_left, lt_add_of_pos_of_le, lt_add_of_pos_of_lt, lt_add_of_pos_of_lt', lt_add_of_pos_right, lt_mul_iff_one_lt_left', lt_mul_iff_one_lt_right', lt_mul_of_le_of_one_lt, lt_mul_of_lt_mul_left, lt_mul_of_lt_mul_right, lt_mul_of_lt_of_one_le, lt_mul_of_lt_of_one_lt, lt_mul_of_lt_of_one_lt', lt_mul_of_one_le_of_lt, lt_mul_of_one_lt_left', lt_mul_of_one_lt_of_le, lt_mul_of_one_lt_of_lt, lt_mul_of_one_lt_of_lt', lt_mul_of_one_lt_right', lt_of_add_lt_add_left, lt_of_add_lt_add_right, lt_of_add_lt_of_nonneg_left, lt_of_add_lt_of_nonneg_right, lt_of_lt_add_of_nonpos_left, lt_of_lt_add_of_nonpos_right, lt_of_lt_mul_of_le_one_left, lt_of_lt_mul_of_le_one_right, lt_of_mul_lt_mul_left', lt_of_mul_lt_mul_right', lt_of_mul_lt_of_one_le_left, lt_of_mul_lt_of_one_le_right, lt_one_of_mul_lt_left, lt_one_of_mul_lt_right, max_add, max_add_add_le_max_add_max, max_mul, max_mul_mul_le_max_mul_max', min_add, min_add_min_le_min_add_add, min_le_max_of_add_le_add, min_le_max_of_mul_le_mul, min_lt_max_of_add_lt_add, min_lt_max_of_mul_lt_mul, min_mul, min_mul_min_le_min_mul_mul', mulLECancellable_mul, mulLECancellable_one, mul_eq_mul_iff_eq_and_eq, mul_eq_one_iff_of_one_le, mul_le_iff_le_one_left', mul_le_iff_le_one_right', mul_le_mul', mul_le_mul_iff_left, mul_le_mul_iff_of_ge, mul_le_mul_iff_right, mul_le_mul_left, mul_le_mul_left', mul_le_mul_right, mul_le_mul_right', mul_le_mul_three, mul_le_of_le_of_le_one, mul_le_of_le_one_left', mul_le_of_le_one_of_le, mul_le_of_le_one_right', mul_le_of_mul_le_left, mul_le_of_mul_le_right, mul_le_one', mul_left_cancel'', mul_left_inj_of_comparable, mul_left_mono, mul_left_strictMono, mul_lt_iff_lt_one_left', mul_lt_iff_lt_one_right', mul_lt_mul_iff_left, mul_lt_mul_iff_right, mul_lt_mul_left, mul_lt_mul_of_le_of_lt, mul_lt_mul_of_lt_of_le, mul_lt_mul_of_lt_of_lt, mul_lt_mul_right, mul_lt_of_le_of_lt_one, mul_lt_of_le_one_of_lt, mul_lt_of_lt_of_le_one, mul_lt_of_lt_of_lt_one, mul_lt_of_lt_of_lt_one', mul_lt_of_lt_one_left', mul_lt_of_lt_one_of_le, mul_lt_of_lt_one_of_lt, mul_lt_of_lt_one_of_lt', mul_lt_of_lt_one_right', mul_lt_of_mul_lt_left, mul_lt_of_mul_lt_right, mul_lt_one, mul_lt_one', mul_lt_one_of_le_of_lt, mul_lt_one_of_lt_of_le, mul_max, mul_min, mul_right_cancel'', mul_right_inj_of_comparable, mul_right_mono, mul_right_strictMono, neg_of_add_lt_left, neg_of_add_lt_right, nonneg_of_le_add_left, nonneg_of_le_add_right, nonpos_of_add_le_left, nonpos_of_add_le_right, one_le_mul, one_le_of_le_mul_left, one_le_of_le_mul_right, one_lt_mul', one_lt_mul'', one_lt_mul_of_le_of_lt', one_lt_mul_of_lt_of_le', one_lt_of_lt_mul_left, one_lt_of_lt_mul_right, pos_of_lt_add_left, pos_of_lt_add_right, trichotomy_of_add_eq_add, trichotomy_of_mul_eq_mul | 384 |
| Total | 390 |