| Metric | Count |
|---|
DefinitionsinstHasDistribNeg, instInvolutiveNeg, instNeg, instSubNegZeroMonoid, neg, negOrderIso, recENNReal, evalERealAdd, evalERealMul | 9 |
TheoremstoEReal_sub, addLECancellable_coe, add_bot, add_eq_bot_iff, add_le_of_forall_lt, add_le_of_le_sub, add_lt_add, add_lt_add_left_coe, add_lt_add_of_lt_of_le, add_lt_add_of_lt_of_le', add_lt_add_right_coe, add_lt_of_lt_sub, add_lt_top, add_ne_bot_iff, add_ne_top, add_ne_top_iff_ne_top_left, add_ne_top_iff_ne_top_right, add_ne_top_iff_ne_top₂, add_ne_top_iff_of_ne_bot_of_ne_top, add_pos, add_pos_of_pos_of_nonneg, add_sub_cancel_left, add_sub_cancel_right, add_top_iff_ne_bot, add_top_of_ne_bot, bot_add, bot_lt_add_iff, bot_mul_bot, bot_mul_coe_of_neg, bot_mul_coe_of_pos, bot_mul_of_neg, bot_mul_of_pos, bot_mul_top, bot_sub, coe_add_top, coe_ennreal_mul_top, coe_mul_bot_of_neg, coe_mul_bot_of_pos, coe_mul_top_of_neg, coe_mul_top_of_pos, coe_neg, coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal, coe_sub, coe_sub_bot, coe_zsmul, ge_of_forall_gt_iff_ge, induction₂_neg_left, induction₂_symm_neg, instNoZeroDivisors, le_add_of_forall_gt, le_neg, le_neg_of_le_neg, le_of_forall_lt_iff_le, le_sub_iff_add_le, left_distrib_of_nonneg, left_distrib_of_nonneg_of_ne_top, lt_neg_comm, lt_neg_of_lt_neg, lt_sub_iff_add_lt, mul_bot_of_neg, mul_bot_of_pos, mul_eq_bot, mul_eq_top, mul_ne_bot, mul_ne_top, mul_neg_iff, mul_nonneg, mul_nonneg_iff, mul_nonpos_iff, mul_pos, mul_pos_iff, mul_top_of_neg, mul_top_of_pos, neg_add, neg_bot, neg_eq_bot_iff, neg_eq_top_iff, neg_eq_zero_iff, neg_le, neg_le_neg_iff, neg_le_of_neg_le, neg_le_zero, neg_lt_comm, neg_lt_neg_iff, neg_lt_of_neg_lt, neg_lt_zero, neg_mul, neg_nonneg, neg_pos, neg_strictAnti, neg_sub, neg_top, nsmul_eq_mul, recENNReal_coe_ennreal, right_distrib_of_nonneg, right_distrib_of_nonneg_of_ne_top, sub_add_cancel, sub_add_cancel_left, sub_add_cancel_right, sub_bot, sub_le_iff_le_add, sub_le_of_le_add, sub_le_of_le_add', sub_le_sub, sub_lt_iff, sub_lt_of_lt_add, sub_lt_of_lt_add', sub_lt_sub_of_lt_of_le, sub_neg, sub_nonneg, sub_nonpos, sub_pos, sub_self, sub_self_le_zero, sub_top, toENNReal_add, toENNReal_add_le, toENNReal_mul, toENNReal_mul', toENNReal_sub, toReal_add, toReal_mul, toReal_neg_eq, toReal_sub, top_add_coe, top_add_iff_ne_bot, top_add_of_ne_bot, top_add_top, top_mul_bot, top_mul_coe_ennreal, top_mul_coe_of_neg, top_mul_coe_of_pos, top_mul_of_neg, top_mul_of_pos, top_mul_top, top_sub, top_sub_bot, top_sub_coe | 138 |
| Total | 147 |