| Metric | Count |
|---|
DefinitionsboundedLimitRecOn, div, limitRecOn, monoid, monoidWithZero, orderTopToTypeSucc, pred, pred_succ_gi, sub | 9 |
Theoremsadd_one_of_aleph0_le, isSuccLimit_ord, noMaxOrder, ordinalPred_eq, ordinalPred_eq, id_le, inj, isSuccLimit, le_apply, le_iff, le_iff_eq, le_set, le_set', limit_le, limit_lt, lt_iff, monotone, refl, strictMono, trans, add_eq_zero_iff, add_le_add_iff_right, add_le_iff, add_le_iff_of_isSuccLimit, add_mul_of_isSuccLimit, add_mul_succ, add_omega0, add_right_cancel, add_sub_add_cancel, add_sub_cancel, add_sub_cancel_of_le, antisymm, boundedLimitRec_limit, boundedLimitRec_succ, boundedLimitRec_zero, bounded_singleton, card_mul, div_add_mod, div_eq_zero_of_lt, div_le, div_le_left, div_le_of_le_mul, div_lt, div_mul_cancel, div_one, div_pos, div_self, div_zero, dvd_add_iff, dvd_antisymm, dvd_iff_mod_eq_zero, dvd_of_mod_eq_zero, enum_succ_eq_top, eq_nat_or_omega0_le, has_succ_of_type_succ_lt, instAddLeftReflectLE, instAddLeftReflectLT, instAddLeftStrictMono, instAddRightReflectLT, instCharZero, instIsLeftCancelAdd, instPosMulStrictMono, isNormal_add_right, isNormal_iff_strictMono_limit, isNormal_mul_right, isSuccLimit_add, isSuccLimit_add_iff, isSuccLimit_add_iff_of_isSuccLimit, isSuccLimit_iff, isSuccLimit_iff_omega0_dvd, isSuccLimit_lift, isSuccLimit_mul, isSuccLimit_mul_left, isSuccLimit_omega0, isSuccLimit_sub, isSuccPrelimit_lift, isSuccPrelimit_zero, le_add_sub, le_div, le_mul_left, le_mul_right, le_of_dvd, le_of_mul_le_mul_left, le_sub_of_add_le, le_sub_of_le, leftDistribClass, left_eq_zero_of_add_eq_zero, lift_add, lift_mul, lift_natCast, lift_ofNat, lift_pred, lift_succ, limitRecOn_limit, limitRecOn_succ, limitRecOn_zero, lt_add_iff, lt_add_iff_of_isSuccLimit, lt_div, lt_mul_div_add, lt_mul_iff_of_isSuccLimit, lt_mul_succ_div, lt_omega0, lt_pred_iff_succ_lt, lt_sub, mk_Iio_ordinal, mod_def, mod_eq_of_lt, mod_eq_zero_of_dvd, mod_le, mod_lt, mod_mod, mod_mod_of_dvd, mod_one, mod_self, mod_zero, mulLeftMono, mulRightMono, mul_add_div, mul_add_div_mul, mul_add_mod_mul, mul_add_mod_self, mul_div_cancel, mul_div_le, mul_div_mul_cancel, mul_le_iff_of_isSuccLimit, mul_le_mul_iff_left, mul_lt_mul_iff_left, mul_lt_mul_of_pos_left, mul_lt_of_lt_div, mul_mod, mul_mod_mul, mul_ne_zero, mul_pos, mul_right_inj, mul_sub, mul_succ, natCast_add_of_omega0_le, natCast_add_omega0, natCast_div, natCast_lt_of_isSuccLimit, natCast_mod, natCast_mod_omega0, natCast_mul, natCast_sub, nat_lt_omega0, noZeroDivisors, not_isSuccLimit_zero, omega0_le, omega0_le_of_isSuccLimit, omega0_ne_zero, omega0_pos, one_add_natCast, one_add_ofNat, one_add_of_omega0_le, one_add_omega0, one_lt_of_isSuccLimit, one_lt_omega0, pred_eq_iff_isSuccPrelimit, pred_eq_of_isSuccPrelimit, pred_le_iff_le_succ, pred_le_self, pred_lt_iff_not_isSuccPrelimit, pred_succ, pred_surjective, pred_zero, right_eq_zero_of_add_eq_zero, self_le_succ_pred, smul_eq_mul, sub_eq_of_add_eq, sub_eq_zero_iff_le, sub_le, sub_le_self, sub_lt_of_le, sub_lt_of_lt_add, sub_ne_zero_iff_lt, sub_self, sub_sub, sub_zero, succ_pred_eq_iff_not_isSuccPrelimit, toType_noMax_of_succ_lt, type_prod_lex, typein_ordinal, zero_div, zero_mod, zero_or_succ_or_isSuccLimit, zero_sub | 187 |
| Total | 196 |
| Name | Category | Theorems |
|---|
boundedLimitRecOn 📖 | CompOp | 3 mathmath: boundedLimitRec_succ, boundedLimitRec_zero, boundedLimitRec_limit
|
div 📖 | CompOp | 28 mathmath: lt_mul_div_add, div_le, div_lt, lt_mul_succ_div, div_add_mod, mul_add_div, div_opow_log_pos, div_self, div_mul_cancel, CNF_ne_zero, div_opow_log_lt, div_le_left, div_eq_zero_of_lt, lt_div, Mathlib.Meta.NormNum.isNat_ordinalDiv, mul_add_div_mul, zero_div, div_pos, div_le_of_le_mul, mul_div_cancel, CNF.ne_zero, mul_div_mul_cancel, le_div, mod_def, div_one, div_zero, mul_div_le, natCast_div
|
limitRecOn 📖 | CompOp | 3 mathmath: limitRecOn_zero, limitRecOn_limit, limitRecOn_succ
|
monoid 📖 | CompOp | 6 mathmath: iSup_pow_natCast, Mathlib.Meta.NormNum.isNat_ordinalNPow, iSup_pow, natCast_pow, type_prod_lex, opow_natCast
|
monoidWithZero 📖 | CompOp | 103 mathmath: opow_mul, lt_omega0_opow_succ, isNormal_mul_right, principal_mul_of_le_two, mul_le_nmul, ONote.nf_repr_split', noZeroDivisors, antisymm, deriv_add_eq_mul_omega0_add, mulRightMono, CNF_foldr, lt_mul_div_add, add_log_le_log_mul, div_le, div_lt, opow_add, lt_mul_succ_div, ONote.repr_mul, div_add_mod, mul_add_div, principal_mul_omega0, nfp_mul_opow_omega0_add, IsInitial.principal_mul, opow_mul_add_pos, mul_le_mul_iff_left, mul_lt_of_lt_div, mul_lt_omega0_opow, natCast_mul_omega0, ONote.split_dvd, dvd_of_mod_eq_zero, mul_mod, principal_mul_ord, log_opow_mul, opow_one_add, opow_dvd_opow, opow_mul_add_lt_opow, smul_eq_mul, iSup_mul_nat, mul_lt_mul_iff_left, instPosMulStrictMono, nfp_mul_eq_opow_omega0, ONote.repr_scale, nfp_mul_zero, principal_mul_omega, mul_eq_right_iff_opow_omega0_dvd, mul_succ, Mathlib.Meta.NormNum.isNat_ordinalMul, opow_mul_add_lt_opow_mul, dvd_iff_mod_eq_zero, mul_lt_mul_of_pos_left, principal_add_mul_of_principal_add, lt_div, ONote.repr_opow_aux₁, iSup_mul_natCast, log_opow_mul_add, natCast_mul, mul_mod_mul, opow_dvd_opow_iff, le_mul_right, add_eq_right_iff_mul_omega0_le, mul_add_div_mul, mul_right_inj, mul_add_mod_self, opow_mul_add_lt_opow_succ, leftDistribClass, lt_omega0_opow, isSuccLimit_mul, CNF.foldr, mulLeftMono, principal_mul_two, deriv_mul_eq_opow_omega0_mul, principal_mul_iff_mul_left_eq, mul_div_cancel, add_mul_of_isSuccLimit, card_mul, mul_le_right_iff_opow_omega0_dvd, mul_sub, principal_mul_omega0_opow_opow, omega0_opow_mul_nat_lt, lt_mul_iff_of_isSuccLimit, add_mul_succ, mul_add_mod_mul, mul_omega0_opow_opow, nfp_mul_one, opow_succ, le_mul_left, opow_mul_add_lt_opow_mul_succ, nfp_add_zero, ONote.scale_opowAux, mul_div_mul_cancel, add_le_right_iff_mul_omega0_le, isSuccLimit_mul_left, lift_mul, mul_omega0, principal_mul_one, le_div, mul_pos, NONote.repr_mul, mod_def, isSuccLimit_iff_omega0_dvd, principal_mul_iff_le_two_or_omega0_opow_opow, mul_div_le, mul_le_iff_of_isSuccLimit
|
orderTopToTypeSucc 📖 | CompOp | 1 mathmath: enum_succ_eq_top
|
pred 📖 | CompOp | 15 mathmath: pred_succ, log_def, lift_pred, pred_le_self, pred_le_iff_le_succ, Order.IsSuccLimit.ordinalPred_eq, pred_surjective, pred_lt_iff_not_isSuccPrelimit, pred_eq_iff_isSuccPrelimit, pred_zero, Order.IsSuccPrelimit.ordinalPred_eq, lt_pred_iff_succ_lt, succ_pred_eq_iff_not_isSuccPrelimit, self_le_succ_pred, pred_eq_of_isSuccPrelimit
|
pred_succ_gi 📖 | CompOp | — |
sub 📖 | CompOp | 25 mathmath: sub_zero, sub_eq_zero_iff_le, zero_opow', zero_sub, natCast_sub, lt_sub, le_sub_of_le, sub_self, add_sub_cancel, sub_lt_of_le, sub_le, Mathlib.Meta.NormNum.isNat_ordinalSub, sub_le_self, le_sub_of_add_le, sub_eq_of_add_eq, mul_sub, add_sub_cancel_of_le, add_sub_add_cancel, sub_lt_of_lt_add, NONote.repr_sub, sub_sub, le_add_sub, mod_def, ONote.repr_sub, isSuccLimit_sub
|