| Metric | Count |
|---|
DefinitionsCauSeq, LimZero, Pos, addGroup, addGroupWithOne, const, equiv, instAdd, instCoeFunForallNat, instCommRingOfIsAbsoluteValue, instInhabited, instIntCast, instLEAbs, instLTAbs, instMaxAbs, instMinAbs, instMul, instNatCast, instNeg, instOne, instPowNat, instPreorderAbs, instSMul, instSub, instZero, inv, ofEq, IsCauSeq | 28 |
Theoremsabv_pos_of_not_limZero, add_apply, add_equiv_add, add_limZero, add_pos, bounded, bounded', cauchy, cauchy₂, cauchy₃, coe_add, coe_const, coe_inf, coe_inv, coe_mul, coe_neg, coe_one, coe_pow, coe_smul, coe_sub, coe_sup, coe_zero, const_add, const_apply, const_equiv, const_inj, const_inv, const_le, const_limZero, const_lt, const_mul, const_neg, const_one, const_pos, const_pow, const_smul, const_sub, const_zero, equiv_def₃, exists_gt, exists_lt, ext, ext_iff, inf_comm, inf_eq_left, inf_eq_right, inf_equiv_inf, inf_idem, inf_le_left, inf_le_right, inf_limZero, instIsScalarTower, inv_apply, inv_aux, inv_mul_cancel, isCauSeq, le_antisymm, le_inf, le_of_eq_of_le, le_of_exists, le_of_le_of_eq, le_sup_left, le_sup_right, le_total, limZero_congr, limZero_sub_rev, lt_inf, lt_irrefl, lt_of_eq_of_lt, lt_of_lt_of_eq, lt_total, lt_trans, mul_apply, mul_equiv_mul, mul_equiv_zero, mul_equiv_zero', mul_inv_cancel, mul_limZero_left, mul_limZero_right, mul_not_equiv_zero, mul_pos, neg_apply, neg_equiv_neg, neg_limZero, not_limZero_of_not_congr_zero, not_limZero_of_pos, of_near, one_apply, one_not_equiv_zero, pos_add_limZero, pow_apply, pow_equiv_pow, rat_inf_continuous_lemma, rat_sup_continuous_lemma, smul_apply, smul_equiv_smul, sub_apply, sub_equiv_sub, sub_limZero, sup_comm, sup_eq_left, sup_eq_right, sup_equiv_sup, sup_idem, sup_inf_distrib_left, sup_inf_distrib_right, sup_le, sup_limZero, sup_lt, trichotomy, zero_apply, zero_limZero, add, bounded, bounded', cauchy₂, cauchy₃, const, mul, neg, of_neg, isCauSeq_neg, rat_add_continuous_lemma, rat_inv_continuous_lemma, rat_mul_continuous_lemma | 125 |
| Total | 153 |
| Name | Category | Theorems |
|---|
LimZero 📖 | MathDef | 18 mathmath: inf_limZero, not_limZero_of_pos, limZero_congr, sub_limZero, const_limZero, limZero_sub_rev, sup_limZero, lim_eq_zero_iff, PadicSeq.not_limZero_const_of_nonzero, mul_limZero_right, not_limZero_of_not_congr_zero, neg_limZero, Completion.mk_eq, mul_limZero_left, add_limZero, Completion.mk_eq_zero, trichotomy, zero_limZero
|
Pos 📖 | MathDef | 6 mathmath: mul_pos, add_pos, pos_add_limZero, trichotomy, Real.mk_pos, const_pos
|
addGroup 📖 | CompOp | — |
addGroupWithOne 📖 | CompOp | — |
const 📖 | CompOp | 32 mathmath: const_one, IsComplete.isComplete, const_lt, lim_mul, Real.cauSeq_converges, const_neg, const_add, lim_const, const_limZero, PadicSeq.not_equiv_zero_const_of_nonzero, const_inj, const_apply, equiv_lim, const_mul, const_sub, const_equiv, const_le, PadicSeq.not_limZero_const_of_nonzero, exists_lt, Real.mk_const, one_not_equiv_zero, const_zero, coe_const, Complex.equiv_limAux, PadicSeq.norm_const, exists_gt, const_inv, const_pow, const_smul, Padic.const_equiv, complete, const_pos
|
equiv 📖 | CompOp | 43 mathmath: mul_equiv_mul, inv_mul_cancel, IsComplete.isComplete, Real.ofCauchy_sup, PadicSeq.ne_zero_iff_nequiv_zero, sub_equiv_sub, pow_equiv_pow, Real.cauSeq_converges, Padic.zero_def, sup_equiv_sup, Real.lt_cauchy, le_antisymm, sup_eq_right, sup_eq_left, inf_equiv_inf, PadicSeq.not_equiv_zero_const_of_nonzero, mul_equiv_zero, equiv_lim, PadicSeq.equiv_zero_of_val_eq_of_equiv_zero, PadicInt.nthHomSeq_mul, Padic.mk_eq, const_equiv, mul_inv_cancel, inf_eq_right, Completion.cau_seq_zero_ne_one, one_not_equiv_zero, neg_equiv_neg, Real.mk_eq, mul_not_equiv_zero, PadicInt.nthHomSeq_add, mul_equiv_zero', smul_equiv_smul, Complex.equiv_limAux, lt_total, PadicInt.nthHomSeq_one, Completion.mk_eq_mk, inf_eq_left, PadicSeq.norm_zero_iff, add_equiv_add, Padic.const_equiv, complete, PadicSeq.eq_zero_iff_equiv_zero, Real.ofCauchy_inf
|
instAdd 📖 | CompOp | 13 mathmath: const_add, lim_add, add_pos, PadicSeq.norm_nonarchimedean, Real.mk_add, Completion.mk_add, pos_add_limZero, coe_add, PadicSeq.add_eq_max_of_ne, PadicInt.nthHomSeq_add, add_limZero, add_apply, add_equiv_add
|
instCoeFunForallNat 📖 | CompOp | — |
instCommRingOfIsAbsoluteValue 📖 | CompOp | — |
instInhabited 📖 | CompOp | — |
instIntCast 📖 | CompOp | — |
instLEAbs 📖 | CompOp | 12 mathmath: le_inf, le_of_exists, le_sup_left, sup_le, const_le, inf_le_right, le_total, le_sup_right, le_of_le_of_eq, le_of_eq_of_le, Real.mk_le, inf_le_left
|
instLTAbs 📖 | CompOp | 12 mathmath: lt_irrefl, const_lt, sup_lt, lt_of_eq_of_lt, Real.lt_cauchy, Real.mk_lt, exists_lt, lt_trans, lt_inf, lt_of_lt_of_eq, lt_total, exists_gt
|
instMaxAbs 📖 | CompOp | 15 mathmath: sup_inf_distrib_right, Real.ofCauchy_sup, sup_idem, sup_lt, coe_sup, sup_equiv_sup, sup_eq_right, sup_eq_left, sup_limZero, le_sup_left, sup_le, sup_comm, le_sup_right, Real.mk_sup, sup_inf_distrib_left
|
instMinAbs 📖 | CompOp | 15 mathmath: sup_inf_distrib_right, inf_limZero, inf_comm, le_inf, inf_equiv_inf, inf_eq_right, inf_le_right, Real.mk_inf, lt_inf, inf_eq_left, sup_inf_distrib_left, inf_idem, coe_inf, inf_le_left, Real.ofCauchy_inf
|
instMul 📖 | CompOp | 19 mathmath: mul_equiv_mul, inv_mul_cancel, mul_apply, lim_mul, mul_pos, Real.mk_mul, mul_equiv_zero, PadicInt.nthHomSeq_mul, const_mul, mul_inv_cancel, mul_limZero_right, Completion.mk_mul, mul_not_equiv_zero, mul_equiv_zero', instIsScalarTower, mul_limZero_left, lim_mul_lim, PadicSeq.norm_mul, coe_mul
|
instNatCast 📖 | CompOp | — |
instNeg 📖 | CompOp | 10 mathmath: const_neg, PadicSeq.norm_neg, neg_limZero, neg_equiv_neg, neg_apply, lim_neg, coe_neg, Completion.mk_neg, Real.mk_neg, trichotomy
|
instOne 📖 | CompOp | 9 mathmath: const_one, inv_mul_cancel, one_apply, Real.mk_one, mul_inv_cancel, coe_one, Completion.cau_seq_zero_ne_one, PadicInt.nthHomSeq_one, PadicSeq.norm_one
|
instPowNat 📖 | CompOp | 5 mathmath: pow_equiv_pow, coe_pow, pow_apply, Completion.mk_pow, const_pow
|
instPreorderAbs 📖 | CompOp | — |
instSMul 📖 | CompOp | 6 mathmath: smul_apply, Completion.mk_smul, instIsScalarTower, smul_equiv_smul, const_smul, coe_smul
|
instSub 📖 | CompOp | 9 mathmath: sub_equiv_sub, sub_apply, sub_limZero, limZero_sub_rev, const_sub, lim_sub, coe_sub, Completion.mk_eq, Completion.mk_sub
|
instZero 📖 | CompOp | 15 mathmath: PadicSeq.ne_zero_iff_nequiv_zero, Padic.zero_def, zero_apply, PadicSeq.not_equiv_zero_const_of_nonzero, mul_equiv_zero, coe_zero, PadicSeq.equiv_zero_of_val_eq_of_equiv_zero, Completion.cau_seq_zero_ne_one, Real.mk_zero, const_zero, mul_not_equiv_zero, mul_equiv_zero', PadicSeq.norm_zero_iff, zero_limZero, PadicSeq.eq_zero_iff_equiv_zero
|
inv 📖 | CompOp | 7 mathmath: inv_mul_cancel, coe_inv, Completion.inv_mk, mul_inv_cancel, inv_apply, const_inv, lim_inv
|
ofEq 📖 | CompOp | — |
| Name | Category | Theorems |
|---|
CauSeq 📖 | CompOp | 122 mathmath: CauSeq.mul_equiv_mul, CauSeq.const_one, CauSeq.inv_mul_cancel, CauSeq.lt_irrefl, CauSeq.IsComplete.isComplete, CauSeq.sup_inf_distrib_right, Real.ofCauchy_sup, CauSeq.sub_equiv_sub, CauSeq.sup_idem, CauSeq.mul_apply, CauSeq.pow_equiv_pow, CauSeq.inf_limZero, CauSeq.const_lt, CauSeq.lim_mul, CauSeq.sup_lt, CauSeq.inf_comm, CauSeq.one_apply, Real.cauSeq_converges, CauSeq.const_neg, Padic.zero_def, Real.mk_one, CauSeq.coe_sup, CauSeq.sup_equiv_sup, CauSeq.lt_of_eq_of_lt, CauSeq.mul_pos, CauSeq.const_add, CauSeq.lim_add, Real.lt_cauchy, CauSeq.add_pos, CauSeq.le_antisymm, CauSeq.sub_apply, Real.mk_lt, CauSeq.sub_limZero, CauSeq.sup_eq_right, CauSeq.smul_apply, CauSeq.zero_apply, CauSeq.le_inf, CauSeq.sup_eq_left, Real.mk_mul, CauSeq.limZero_sub_rev, CauSeq.inf_equiv_inf, PadicSeq.not_equiv_zero_const_of_nonzero, CauSeq.mul_equiv_zero, Real.mk_add, CauSeq.sup_limZero, CauSeq.equiv_lim, CauSeq.Completion.mk_smul, CauSeq.coe_zero, CauSeq.le_of_exists, CauSeq.Completion.mk_add, CauSeq.le_sup_left, CauSeq.const_mul, CauSeq.sup_le, CauSeq.const_sub, CauSeq.const_equiv, CauSeq.const_le, CauSeq.lim_sub, CauSeq.mul_inv_cancel, CauSeq.sup_comm, CauSeq.inf_eq_right, CauSeq.pos_add_limZero, CauSeq.coe_one, CauSeq.mul_limZero_right, CauSeq.coe_sub, CauSeq.inf_le_right, CauSeq.Completion.mk_mul, CauSeq.exists_lt, CauSeq.Completion.cau_seq_zero_ne_one, CauSeq.coe_pow, CauSeq.one_not_equiv_zero, Real.mk_zero, CauSeq.lt_trans, CauSeq.pow_apply, CauSeq.le_total, CauSeq.coe_add, CauSeq.neg_limZero, CauSeq.le_sup_right, Real.mk_inf, CauSeq.const_zero, CauSeq.neg_equiv_neg, Real.mk_eq, Real.mk_sup, CauSeq.mul_not_equiv_zero, CauSeq.lt_inf, CauSeq.lt_of_lt_of_eq, CauSeq.mul_equiv_zero', CauSeq.instIsScalarTower, CauSeq.smul_equiv_smul, CauSeq.Completion.mk_eq, Complex.equiv_limAux, CauSeq.neg_apply, CauSeq.lim_neg, CauSeq.lt_total, CauSeq.mul_limZero_left, CauSeq.add_limZero, CauSeq.coe_neg, CauSeq.Completion.mk_neg, CauSeq.Completion.mk_eq_mk, CauSeq.exists_gt, CauSeq.inf_eq_left, Real.mk_neg, CauSeq.trichotomy, CauSeq.Completion.mk_pow, CauSeq.Completion.mk_sub, CauSeq.le_of_le_of_eq, CauSeq.le_of_eq_of_le, CauSeq.add_apply, CauSeq.add_equiv_add, CauSeq.const_pow, CauSeq.sup_inf_distrib_left, CauSeq.inf_idem, CauSeq.lim_mul_lim, CauSeq.const_smul, Padic.const_equiv, Real.mk_le, CauSeq.complete, CauSeq.coe_smul, CauSeq.zero_limZero, CauSeq.coe_inf, CauSeq.inf_le_left, Real.ofCauchy_inf, CauSeq.coe_mul
|
IsCauSeq 📖 | MathDef | 73 mathmath: PadicInt.isCauSeq_nthHom, CauSeq.inv_aux, Padic.complete', IsCauSeq.of_decreasing_bounded, CauSeq.abv_pos_of_not_limZero, CauSeq.cauchy₂, CauSeq.mul_apply, CauSeq.ext_iff, Complex.isCauSeq_conj, Padic.exi_rat_seq_conv_cauchy, IsCauSeq.of_abv_le, CauSeq.one_apply, IsCauSeq.const, Real.of_near, CauSeq.cauchy, CauSeq.coe_sup, IsCauSeq.of_abv, PadicSeq.lift_index_left_left, CauSeq.bounded', padicNormE.defn, CauSeq.sub_apply, PadicSeq.lift_index_right, CauSeq.isCauSeq, CauSeq.smul_apply, CauSeq.zero_apply, Complex.isCauSeq_norm_exp, CauSeq.coe_inv, IsCauSeq.geo_series, CauSeq.of_near, CauSeq.const_apply, CauSeq.coe_zero, IsCauSeq.neg, Padic.complete'', RCLike.isCauSeq_norm, CauSeq.tendsto_limit, RCLike.isCauSeq_im, CauSeq.cauchySeq, Padic.exi_rat_seq_conv, CauSeq.coe_one, isCauSeq_iff_cauchySeq, CauSeq.coe_sub, PadicSeq.stationaryPoint_spec, IsCauSeq.of_neg, CauSeq.coe_pow, CauSeq.pow_apply, PadicSeq.lift_index_left, CauSeq.inv_apply, CauSeq.coe_add, Complex.isCauSeq_im, IsCauSeq.mul, PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub, IsCauSeq.geo_series_const, CauSeq.coe_const, Complex.isCauSeq_norm, CauSeq.neg_apply, CauSeq.coe_neg, CauSeq.equiv_def₃, isCauSeq_neg, CauSeq.add_apply, IsCauSeq.of_mono_bounded, PadicSeq.stationary, CauchySeq.isCauSeq, Complex.isCauSeq_exp, IsCauSeq.add, RCLike.isCauSeq_re, CauSeq.bounded, Complex.isCauSeq_re, Real.isCauSeq_iff_lift, CauSeq.coe_smul, CauSeq.coe_inf, CauSeq.cauchy₃, IsCauSeq.series_ratio_test, CauSeq.coe_mul
|