| Metric | Count |
|---|
DefinitionspartialProd, partialSum, finFunctionFinEquiv, finPiFinEquiv, finSigmaFinEquiv | 5 |
Theoremsadd_sum_removeNth, inv_partialProd_mul_eq_contractNth, mul_prod_removeNth, neg_partialSum_add_eq_contractNth, partialProd_contractNth, partialProd_init, partialProd_left_inv, partialProd_right_inv, partialProd_succ, partialProd_succ', partialProd_zero, partialSum_contractNth, partialSum_init, partialSum_left_neg, partialSum_right_neg, partialSum_succ, partialSum_succ', partialSum_zero, prod_Icc_cast, prod_Icc_castAdd, prod_Icc_castLE, prod_Icc_castSucc, prod_Icc_succ, prod_Ici_cast, prod_Ici_succ, prod_Ico_cast, prod_Ico_castAdd, prod_Ico_castLE, prod_Ico_castSucc, prod_Ico_succ, prod_Iic_cast, prod_Iic_castAdd, prod_Iic_castLE, prod_Iic_castSucc, prod_Iio_cast, prod_Iio_castAdd, prod_Iio_castLE, prod_Iio_castSucc, prod_Ioc_cast, prod_Ioc_castAdd, prod_Ioc_castLE, prod_Ioc_castSucc, prod_Ioc_succ, prod_Ioi_cast, prod_Ioi_succ, prod_Ioi_zero, prod_Ioo_cast, prod_Ioo_castAdd, prod_Ioo_castLE, prod_Ioo_castSucc, prod_Ioo_succ, prod_congr', prod_cons, prod_const, prod_insertNth, prod_ofFn, prod_prod_eq_prod_triangle_mul, prod_snoc, prod_trunc, prod_uIcc_cast, prod_uIcc_castAdd, prod_uIcc_castLE, prod_uIcc_castSucc, prod_uIcc_succ, prod_univ_add, prod_univ_castSucc, prod_univ_def, prod_univ_eight, prod_univ_five, prod_univ_four, prod_univ_fun_getElem, prod_univ_getElem, prod_univ_one, prod_univ_seven, prod_univ_six, prod_univ_succ, prod_univ_succAbove, prod_univ_three, prod_univ_two, prod_univ_two', prod_univ_zero, sum_Icc_cast, sum_Icc_castAdd, sum_Icc_castLE, sum_Icc_castSucc, sum_Icc_succ, sum_Ici_cast, sum_Ici_succ, sum_Ico_cast, sum_Ico_castAdd, sum_Ico_castLE, sum_Ico_castSucc, sum_Ico_succ, sum_Iic_cast, sum_Iic_castAdd, sum_Iic_castLE, sum_Iic_castSucc, sum_Iio_cast, sum_Iio_castAdd, sum_Iio_castLE, sum_Iio_castSucc, sum_Ioc_cast, sum_Ioc_castAdd, sum_Ioc_castLE, sum_Ioc_castSucc, sum_Ioc_succ, sum_Ioi_cast, sum_Ioi_succ, sum_Ioi_zero, sum_Ioo_cast, sum_Ioo_castAdd, sum_Ioo_castLE, sum_Ioo_castSucc, sum_Ioo_succ, sum_congr', sum_cons, sum_const, sum_insertNth, sum_neg_one_pow, sum_ofFn, sum_pow_mul_eq_add_pow, sum_snoc, sum_sum_eq_sum_triangle_add, sum_trunc, sum_uIcc_cast, sum_uIcc_castAdd, sum_uIcc_castLE, sum_uIcc_castSucc, sum_uIcc_succ, sum_univ_add, sum_univ_castSucc, sum_univ_def, sum_univ_eight, sum_univ_five, sum_univ_four, sum_univ_fun_getElem, sum_univ_getElem, sum_univ_one, sum_univ_seven, sum_univ_six, sum_univ_succ, sum_univ_succAbove, sum_univ_three, sum_univ_two, sum_univ_two', sum_univ_zero, prod_range, sum_range, alternatingProd_eq_finset_prod, alternatingSum_eq_finset_sum, prod_ofFn, prod_take_ofFn, sum_ofFn, sum_take_ofFn, finFunctionFinEquiv_apply, finFunctionFinEquiv_apply_val, finFunctionFinEquiv_single, finFunctionFinEquiv_symm_apply_val, finPiFinEquiv_apply, finPiFinEquiv_single, finSigmaFinEquiv_apply, finSigmaFinEquiv_one | 162 |
| Total | 167 |