| Metric | Count |
|---|
| Definitions | 0 |
Theoremsconst_mul, mul_const, le_self_pow_of_pos, one_le_invâ, one_lt_mul, pow_le_pow_right_of_le_one_or_one_le, mul_lt_mul'', mul_lt_mul_of_nonneg, mul_nonneg, mul_pos, neg_of_mul_neg_left, neg_of_mul_neg_right, const_mul, mul, mul_const, mul_strictMono, mul, toMulPosStrictMono, of_posMulReflectLT_of_mulPosMono, toMulPosReflectLT, toMulPosReflectLE, toMulPosStrictMono, toMulPosMono, toPosMulStrictMono, toPosMulReflectLT, toPosMulReflectLE, toPosMulStrictMono, toPosMulMono, inv_nonneg, inv_pos, mul_lt_mul_of_nonneg, mul_nonneg, mul_pos, neg_of_mul_neg_left, neg_of_mul_neg_right, const_mul, mul_const, const_mul, mul, mul_const, mul_monotone, div_le_commâ, div_le_div_iff_of_pos_left, div_le_div_iff_of_pos_right, div_le_div_iffâ, div_le_div_of_nonneg_left, div_le_div_of_nonneg_right, div_le_divâ, div_le_iffâ, div_le_iffâ', div_le_of_le_mulâ, div_le_one_of_leâ, div_le_oneâ, div_lt_commâ, div_lt_div_iff_of_pos_left, div_lt_div_iff_of_pos_right, div_lt_div_iffâ, div_lt_div_of_pos_left, div_lt_div_of_pos_right, div_lt_divâ, div_lt_divâ', div_lt_iffâ, div_lt_iffâ', div_lt_oneâ, div_nonneg, div_nonpos_of_nonneg_of_nonpos, div_nonpos_of_nonpos_of_nonneg, div_pos, div_self_le_one, inv_antiâ, inv_le_commâ, inv_le_iff_one_le_mulâ, inv_le_iff_one_le_mulâ', inv_le_invâ, inv_le_of_inv_leâ, inv_le_one_iffâ, inv_le_one_of_one_leâ, inv_le_oneâ, inv_lt_commâ, inv_lt_iff_one_lt_mulâ, inv_lt_iff_one_lt_mulâ', inv_lt_invâ, inv_lt_of_inv_ltâ, inv_lt_one_iffâ, inv_lt_one_of_one_ltâ, inv_lt_oneâ, inv_lt_zero, inv_mul_le_iffâ, inv_mul_le_iffâ', inv_mul_le_of_le_mulâ, inv_mul_le_one, inv_mul_le_one_of_leâ, inv_mul_le_oneâ, inv_mul_left_le, inv_mul_lt_iffâ, inv_mul_lt_iffâ', inv_mul_lt_oneâ, inv_mul_right_le, inv_neg'', inv_nonneg, inv_nonneg_of_nonneg, inv_nonpos, inv_pos, inv_pos_of_pos, inv_strictAntiâ, le_div_commâ, le_div_iffâ, le_div_iffâ', le_inv_commâ, le_inv_mul_iffâ, le_inv_mul_iffâ', le_inv_mul_left, le_inv_mul_right, le_inv_of_le_invâ, le_mul_div_mul_left, le_mul_div_mul_right, le_mul_iff_one_le_left, le_mul_iff_one_le_right, le_mul_inv_iffâ, le_mul_inv_iffâ', le_mul_inv_left, le_mul_inv_right, le_mul_of_one_le_left, le_mul_of_one_le_right, le_of_pow_le_pow_leftâ, le_self_powâ, lt_div_commâ, lt_div_iffâ, lt_div_iffâ', lt_inv_commâ, lt_inv_mul_iffâ, lt_inv_mul_iffâ', lt_inv_of_lt_invâ, lt_mul_iff_one_lt_left, lt_mul_iff_one_lt_right, lt_mul_inv_iffâ, lt_mul_inv_iffâ', lt_mul_left, lt_mul_of_one_lt_left, lt_mul_of_one_lt_right, lt_mul_right, lt_mul_self, lt_of_mul_self_lt_mul_selfâ, lt_of_pow_lt_pow_leftâ, lt_self_powâ, monotone_mul_left_of_nonneg, monotone_mul_right_of_nonneg, mulPosMono_iff_covariant_pos, mulPosMono_iff_mulPosStrictMono, mulPosReflectLE_iff_mulPosReflectLT, mulPosReflectLT_iff_contravariant_pos, mul_div_mul_left_le, mul_div_mul_right_le, mul_eq_mul_iff_eq_and_eq_of_pos, mul_eq_mul_iff_eq_and_eq_of_pos', mul_inv_le_iffâ, mul_inv_le_iffâ', mul_inv_le_of_le_mulâ, mul_inv_le_one, mul_inv_le_one_of_leâ, mul_inv_left_le, mul_inv_lt_iffâ, mul_inv_lt_iffâ', mul_inv_right_le, mul_le_iff_le_one_left, mul_le_iff_le_one_right, mul_le_of_le_divâ, mul_le_of_le_inv_mulâ, mul_le_of_le_mul_invâ, mul_le_of_le_one_left, mul_le_of_le_one_right, mul_le_oneâ, mul_left_cancel_iff_of_pos, mul_lt_iff_lt_one_left, mul_lt_iff_lt_one_right, mul_lt_mul'', mul_lt_mul_of_nonneg, mul_lt_of_lt_one_left, mul_lt_of_lt_one_right, mul_lt_one_of_nonneg_of_lt_one_left, mul_lt_one_of_nonneg_of_lt_one_right, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg, mul_nonneg, mul_nonpos_of_nonneg_of_nonpos, mul_nonpos_of_nonpos_of_nonneg, mul_pos, mul_pos_iff_of_pos_left, mul_pos_iff_of_pos_right, mul_right_cancel_iff_of_pos, mul_self_le_mul_self, mul_self_lt_mul_self, neg_iff_neg_of_mul_pos, neg_of_div_neg_left, neg_of_div_neg_right, neg_of_mul_neg_left, neg_of_mul_neg_right, neg_of_mul_pos_left, neg_of_mul_pos_right, one_div_neg, one_div_nonneg, one_div_nonpos, one_div_pos, one_le_divâ, one_le_inv_iffâ, one_le_inv_mulâ, one_le_invâ, one_le_mul_of_one_le_of_one_le, one_le_of_le_mul_leftâ, one_le_of_le_mul_rightâ, one_le_pow_iff_of_nonneg, one_le_powâ, one_le_sq_iffâ, one_le_zpow_iff_right_of_lt_oneâ, one_le_zpow_iff_rightâ, one_le_zpow_of_nonposâ, one_le_zpowâ, one_lt_divâ, one_lt_inv_iffâ, one_lt_inv_mulâ, one_lt_invâ, 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â, one_lt_pow_iff_of_nonneg, one_lt_powâ, one_lt_sq_iffâ, one_lt_zpow_iff_right_of_lt_oneâ, one_lt_zpow_iff_rightâ, one_lt_zpow_of_negâ, one_lt_zpowâ, posMulMono_iff_covariant_pos, posMulMono_iff_posMulStrictMono, posMulReflectLE_iff_posMulReflectLT, posMulReflectLT_iff_contravariant_pos, pos_and_pos_or_neg_and_neg_of_mul_pos, pos_iff_pos_of_mul_pos, pos_of_mul_pos_left, pos_of_mul_pos_right, pow_eq_one_iff_of_nonneg, pow_le_of_le_one, pow_le_one_iff_of_nonneg, pow_le_oneâ, pow_le_pow_iff_leftâ, pow_le_pow_iff_right_of_lt_oneâ, pow_le_pow_iff_rightâ, pow_le_pow_leftâ, pow_le_pow_of_le_one, pow_le_pow_rightâ, pow_left_injâ, pow_left_monotoneOn, pow_left_strictMonoOnâ, pow_lt_one_iff_of_nonneg, pow_lt_oneâ, pow_lt_pow_iff_leftâ, pow_lt_pow_iff_right_of_lt_oneâ, pow_lt_pow_iff_rightâ, pow_lt_pow_leftâ, pow_lt_pow_right_of_lt_oneâ, pow_lt_pow_rightâ, pow_lt_self_of_lt_oneâ, pow_nonneg, pow_pos, pow_right_antiâ, pow_right_injectiveâ, pow_right_injâ, pow_right_monoâ, pow_right_strictAntiâ, pow_right_strictMonoâ, pow_succ_nonneg, pow_succ_pos, sq_eq_sqâ, sq_le, sq_le_one_iffâ, sq_le_sqâ, sq_lt_one_iffâ, sq_lt_sqâ, sq_pos_of_pos, strictMonoOn_mul_self, strictMono_mul_left_of_pos, strictMono_mul_right_of_pos, zero_pow_le_one, zpow_eq_one_iff_rightâ, zpow_le_one_iff_right_of_lt_oneâ, zpow_le_one_iff_rightâ, zpow_le_one_of_nonposâ, zpow_le_oneâ, zpow_le_zpow_iff_leftâ, zpow_le_zpow_iff_right_of_lt_oneâ, zpow_le_zpow_iff_rightâ, zpow_le_zpow_leftâ, zpow_le_zpow_right_of_le_oneâ, zpow_le_zpow_rightâ, zpow_left_injOnâ, zpow_left_injâ, zpow_left_monoOnâ, zpow_left_strictMonoOnâ, zpow_lt_one_iff_right_of_lt_oneâ, zpow_lt_one_iff_rightâ, zpow_lt_one_of_negâ, zpow_lt_oneâ, zpow_lt_zpow_iff_leftâ, zpow_lt_zpow_iff_right_of_lt_oneâ, zpow_lt_zpow_iff_rightâ, zpow_lt_zpow_leftâ, zpow_lt_zpow_right_of_lt_oneâ, zpow_lt_zpow_rightâ, zpow_nonneg, zpow_pos, zpow_right_antiâ, zpow_right_injectiveâ, zpow_right_injâ, zpow_right_monoâ, zpow_right_strictAntiâ, zpow_right_strictMonoâ | 317 |
| Total | 317 |