| Metric | Count |
|---|
DefinitionsinstDivInvOneMonoid, instInvolutiveInv, mulLeftOrderIso, mulRightOrderIso, orderIsoIicCoe, orderIsoIicOneBirational, orderIsoUnitIntervalBirational, invENNReal | 8 |
Theoremsinv_ne_top, Ioo_zero_top_eq_iUnion_Ico_zpow, add_div, add_halves, add_thirds, coe_div, coe_div_le, coe_inv, coe_inv_le, coe_inv_two, coe_zpow, div_add_div_same, div_div_cancel, div_div_cancel', div_eq_div_iff, div_eq_inv_mul, div_eq_one_iff, div_eq_top, div_eq_zero_iff, div_le_div, div_le_div_left, div_le_div_right, div_le_iff, div_le_iff', div_le_iff_le_mul, div_le_of_le_mul, div_le_of_le_mul', div_lt_div_iff_left, div_lt_div_iff_right, div_lt_div_left, div_lt_div_right, div_lt_iff, div_lt_of_lt_mul, div_lt_of_lt_mul', div_lt_top, div_mul, div_mul_cancel, div_mul_cancel', div_ne_top, div_ne_zero, div_pos, div_pos_iff, div_right_comm, div_self, div_self_le_one, div_top, div_zero, eq_div_iff, eq_inv_of_mul_eq_one_left, eq_of_forall_le_nnreal_iff, eq_of_forall_nnreal_iff, eq_of_forall_nnreal_le_iff, eq_top_of_forall_nnreal_le, exists_inv_nat_lt, exists_inv_two_pow_lt, exists_mem_Ico_zpow, exists_mem_Ioc_zpow, exists_nat_mul_gt, exists_nat_pos_inv_mul_lt, exists_nat_pos_mul_gt, exists_nnreal_pos_mul_lt, exists_pos_mul_lt, half_le_self, half_lt_self, half_pos, iInf_div, iInf_div', iInf_div_of_ne, iInf_mul, iInf_mul', iInf_mul_iInf, iInf_mul_of_ne, iSup_div, iSup_mul, iSup_mul_le, inv_div, inv_eq_one, inv_eq_top, inv_eq_zero, inv_iInf, inv_iSup, inv_le_iff_inv_le, inv_le_iff_le_mul, inv_le_inv, inv_le_inv', inv_le_one, inv_lt_iff_inv_lt, inv_lt_inv, inv_lt_inv', inv_lt_one, inv_lt_top, inv_mul_cancel, inv_mul_cancel_left, inv_mul_cancel_left', inv_mul_cancel_right, inv_mul_cancel_right', inv_mul_le_iff, inv_mul_le_one, inv_mul_ne_top, inv_ne_top, inv_ne_zero, inv_pos, inv_pow, inv_sInf, inv_sSup, inv_strictAnti, inv_three_add_inv_three, inv_top, inv_two_add_inv_two, inv_zero, inv_zpow, inv_zpow', isUnit_iff, le_div_iff_mul_le, le_iInf_mul, le_iInf_mul_iInf, le_inv_iff_le_inv, le_inv_iff_mul_le, le_mul_of_forall_lt, le_of_forall_nnreal_lt, le_of_forall_pos_nnreal_lt, lt_div_iff_mul_lt, lt_inv_iff_lt_inv, monotone_zpow, mulLeftOrderIso_apply, mulLeftOrderIso_symm_apply, mulLeftOrderIso_toEquiv, mulRightOrderIso_apply, mulRightOrderIso_symm_apply, mulRightOrderIso_toEquiv, mul_comm_div, mul_div_cancel, mul_div_cancel', mul_div_cancel_right, mul_div_cancel_right', mul_div_le, mul_div_mul_comm, mul_div_mul_left, mul_div_mul_right, mul_div_right_comm, mul_iInf, mul_iInf', mul_iInf_of_ne, mul_iSup, mul_inv, mul_inv_cancel, mul_inv_cancel_left, mul_inv_cancel_left', mul_inv_cancel_right, mul_inv_cancel_right', mul_inv_le_iff, mul_inv_le_one, mul_inv_ne_top, mul_le_iff_le_inv, mul_le_of_forall_lt, mul_le_of_le_div, mul_le_of_le_div', mul_lt_of_lt_div, mul_lt_of_lt_div', mul_sSup, ofReal_div_of_pos, ofReal_inv_of_pos, one_half_lt_one, one_le_inv, one_lt_inv, one_sub_inv_two, orderIsoIicCoe_apply_coe, orderIsoIicCoe_symm_apply_coe, orderIsoIicOneBirational_apply_coe, orderIsoIicOneBirational_symm_apply, orderIsoUnitIntervalBirational_apply_coe, sSup_div, sSup_mul, smul_iSup, smul_sSup, sub_div, sub_half, toNNReal_div, toNNReal_inv, toReal_div, toReal_inv, top_div, top_div_coe, top_div_of_lt_top, top_div_of_ne_top, top_zpow_def, zero_div, zero_zpow_def, zpow_add, zpow_le_of_le, zpow_le_one_of_nonpos, zpow_lt_top, zpow_ne_top, zpow_neg, zpow_pos, zpow_sub, invENNReal_apply, invENNReal_symm_apply | 198 |
| Total | 206 |