| Metric | Count |
|---|
DefinitionsAdicCauchySequence, instAdd, instAddCommGroup, instCoeFunForallNat, instModule, instNeg, instSMul, instSMulInt, instSMulNat, instSub, instZero, mk, submodule, IsAdicCauchy, eval, incl, instAdd, instAddCommGroup, instModuleOfIsScalarTower, instNeg, instSMul, instSub, instZero, mk, of, ofLinearEquiv, submodule, transitionMap, Hausdorffification, of, IsAdicComplete, extend, IsHausdorff, IsPrecomplete | 34 |
Theoremsadd_apply, ext, ext_iff, mk_coe, mk_eq_mk, smul_apply, sub_apply, zero_apply, coe_eval, eval_apply, eval_comp_of, eval_lift, eval_lift_apply, eval_of, eval_surjective, ext, ext_iff, incl_apply, induction_on, instIsCentralScalar, instIsHausdorff, instIsScalarTower, instSMulCommClass, isAdicCauchy_iff, mk_apply_coe, mk_surjective, mk_zero_of, ofLinearEquiv_apply, ofLinearEquiv_symm_of, of_apply, of_bijective, of_bijective_iff, of_inj, of_injective, of_injective_iff, of_ofLinearEquiv_symm, of_surjective, of_surjective_iff, pow_smul_top_le_ker_eval, range_eval, transitionMap_comp_eval, transitionMap_comp_eval_apply, val_add, val_add_apply, val_apply_mem_smul_top_iff, val_neg, val_neg_apply, val_smul, val_smul_apply, val_sub, val_sub_apply, val_sum, val_sum_apply, val_zero, val_zero_apply, induction_on, instIsHausdorff, lift_comp_of, lift_eq, lift_of, eq_lift, extend_eq, factorPow_comp_eq_of_factorPow_comp_succ_eq, factorPow_comp_extend, mkQ_comp_lift, mk_lift, of_comp_lift, of_lift, bot, eq_lift, le_jacobson_bot, map_algebraMap_iff, mkQ_comp_lift, mk_lift, of_comp_lift, of_lift, of_subsingleton, subsingleton, toIsHausdorff, toIsPrecomplete, funext, funext', bot, eq_iff_smodEq, funext, funext', haus, haus', iInf_pow_smul, map_algebraMap_iff, of_map, of_subsingleton, subsingleton, bot, map_algebraMap_iff, of_subsingleton, prec, prec', top, isAdicComplete_iff, isHausdorff_iff, isPrecomplete_iff | 102 |
| Total | 136 |
| Name | Category | Theorems |
|---|
AdicCauchySequence 📖 | CompOp | 20 mathmath: mk_zero_of, map_ext'_iff, AdicCauchySequence.zero_apply, mkₐ_apply_coe, AdicCauchySequence.map_zero, AdicCauchySequence.add_apply, AdicCauchySequence.smul_apply, AdicCauchySequence.map_id, AdicCauchySequence.sub_apply, map_mk, AdicCauchySequence.map_apply_coe, mk_surjective, map_ext''_iff, AdicCauchySequence.map_comp_apply, mul_apply, one_apply, AdicCauchySequence.map_comp, evalₐ_mk, evalₐ_mkₐ, mk_apply_coe
|
IsAdicCauchy 📖 | MathDef | 17 mathmath: AdicCauchySequence.mk_eq_mk, AdicCauchySequence.zero_apply, mkₐ_apply_coe, isAdicCauchy_iff, AdicCauchySequence.add_apply, AdicCauchySequence.smul_apply, AdicCauchySequence.ext_iff, AdicCauchySequence.sub_apply, smul_mk, Ideal.mk_eq_mk, AdicCauchySequence.map_apply_coe, AdicCauchySequence.mk_coe, mul_apply, one_apply, evalₐ_mk, evalₐ_mkₐ, mk_apply_coe
|
eval 📖 | CompOp | 15 mathmath: factor_eval_eq_evalₐ, range_eval, transitionMap_comp_eval, coe_eval, pow_smul_top_eq_ker_eval, pow_smul_top_le_ker_eval, mk_smul_top_ofAlgEquiv_symm, factor_eval_liftRingHom, restrictScalars_range_ofPowSMul_eq_ker_eval, factor_evalₐ_eq_eval, eval_of, eval_surjective, eval_apply, eval_comp_of, eval_lift
|
incl 📖 | CompOp | 1 mathmath: incl_apply
|
instAdd 📖 | CompOp | 2 mathmath: val_add_apply, val_add
|
instAddCommGroup 📖 | CompOp | 87 mathmath: of_surjective_iff, algebraMap_apply, mk_zero_of, map_val_apply, of_ofAlgEquiv_symm, incl_apply, map_ext'_iff, ofTensorProduct_surjective_of_finite, pi_apply_coe, map_injective, ofPowSMul_ofValEqZero, factor_eval_eq_evalₐ, IsAdicComplete.of_liftRingHom, sumInv_apply, sum_lof, map_comp_apply, val_sum, IsAdicComplete.of_lift, map_comp, range_eval, transitionMap_comp_eval, map_id, instIsHausdorff, sumInv_comp_sum, coe_eval, coe_ofTensorProductEquivOfFiniteNoetherian, ofTensorProductEquivOfFiniteNoetherian_symm_of, ofTensorProduct_bijective_of_finite_of_isNoetherian, of_bijective_iff, ofPowSMul_injective, isAdicComplete, IsAdicComplete.of_comp_lift, ofTensorProduct_bijective_of_pi_of_fintype, map_mk, pow_smul_top_eq_ker_eval, ofAlgEquiv_apply, of_surjective, ofPowSMul_val_apply_eq_zero, sum_of, mk_surjective, pow_smul_top_le_ker_eval, map_ext''_iff, congr_symm_apply, of_ofLinearEquiv_symm, kerProj_of, evalOneₐ_of, IsAdicComplete.StrictMono.of_comp_lift, mk_smul_top_ofAlgEquiv_symm, tensor_map_id_left_eq_map, factor_eval_liftRingHom, of_inj, ofTensorProduct_tmul, map_exact, of_injective, restrictScalars_range_ofPowSMul_eq_ker_eval, ofTensorProductEquivOfFiniteNoetherian_apply, sumEquivOfFintype_apply, of_bijective, evalₐ_of, factor_evalₐ_eq_eval, eval_of, map_zero, component_sumInv, evalₐ_mk, piEquivOfFintype_apply, IsAdicComplete.StrictMono.of_lift, ofTensorProduct_naturality, ofLinearEquiv_apply, mk_apply_coe, congr_apply, of_injective_iff, eval_lift_apply, eval_surjective, ofPowSMul_val_apply, sumEquivOfFintype_symm_apply, eval_apply, piEquivFin_apply, ofLinearEquiv_symm_of, val_sum_apply, map_of, map_surjective_of_mkQ_comp_surjective, of_apply, map_surjective, eval_comp_of, sum_comp_sumInv, eval_lift, ofAlgEquiv_symm_of
|
instModuleOfIsScalarTower 📖 | CompOp | 61 mathmath: of_surjective_iff, algebraMap_apply, mk_zero_of, of_ofAlgEquiv_symm, incl_apply, map_ext'_iff, ofTensorProduct_surjective_of_finite, factor_eval_eq_evalₐ, IsAdicComplete.of_liftRingHom, IsAdicComplete.of_lift, range_eval, transitionMap_comp_eval, instIsHausdorff, coe_eval, coe_ofTensorProductEquivOfFiniteNoetherian, ofTensorProductEquivOfFiniteNoetherian_symm_of, ofTensorProduct_bijective_of_finite_of_isNoetherian, of_bijective_iff, isAdicComplete, IsAdicComplete.of_comp_lift, ofTensorProduct_bijective_of_pi_of_fintype, map_mk, pow_smul_top_eq_ker_eval, ofAlgEquiv_apply, of_surjective, mk_surjective, pow_smul_top_le_ker_eval, map_ext''_iff, of_ofLinearEquiv_symm, kerProj_of, evalOneₐ_of, IsAdicComplete.StrictMono.of_comp_lift, mk_smul_top_ofAlgEquiv_symm, tensor_map_id_left_eq_map, factor_eval_liftRingHom, of_inj, ofTensorProduct_tmul, of_injective, restrictScalars_range_ofPowSMul_eq_ker_eval, ofTensorProductEquivOfFiniteNoetherian_apply, of_bijective, evalₐ_of, factor_evalₐ_eq_eval, eval_of, evalₐ_mk, IsAdicComplete.StrictMono.of_lift, ofTensorProduct_naturality, ofLinearEquiv_apply, mk_apply_coe, of_injective_iff, eval_lift_apply, tensor_map_id_left_injective_of_injective, eval_surjective, eval_apply, flat_of_isNoetherian, ofLinearEquiv_symm_of, map_of, of_apply, eval_comp_of, eval_lift, ofAlgEquiv_symm_of
|
instNeg 📖 | CompOp | 2 mathmath: val_neg_apply, val_neg
|
instSMul 📖 | CompOp | 7 mathmath: instIsScalarTower_1, val_smul, instIsCentralScalar, restrictScalars_range_ofPowSMul_eq_ker_eval, instIsScalarTower, instSMulCommClass, val_smul_apply
|
instSub 📖 | CompOp | 2 mathmath: val_sub_apply, val_sub
|
instZero 📖 | CompOp | 4 mathmath: mk_zero_of, map_exact, val_zero, val_zero_apply
|
mk 📖 | CompOp | — |
of 📖 | CompOp | 28 mathmath: of_surjective_iff, algebraMap_apply, of_ofAlgEquiv_symm, IsAdicComplete.of_liftRingHom, IsAdicComplete.of_lift, ofTensorProductEquivOfFiniteNoetherian_symm_of, of_bijective_iff, IsAdicComplete.of_comp_lift, ofAlgEquiv_apply, of_surjective, of_ofLinearEquiv_symm, kerProj_of, evalOneₐ_of, IsAdicComplete.StrictMono.of_comp_lift, of_inj, ofTensorProduct_tmul, of_injective, of_bijective, evalₐ_of, eval_of, IsAdicComplete.StrictMono.of_lift, ofLinearEquiv_apply, of_injective_iff, ofLinearEquiv_symm_of, map_of, of_apply, eval_comp_of, ofAlgEquiv_symm_of
|
ofLinearEquiv 📖 | CompOp | 3 mathmath: of_ofLinearEquiv_symm, ofLinearEquiv_apply, ofLinearEquiv_symm_of
|
submodule 📖 | CompOp | — |
transitionMap 📖 | CompOp | 7 mathmath: transitionMap_comp_eval, transitionMap_comp_reduceModIdeal, transitionMap_map_pow, transitionMap_ideal_mk, transitionMap_map_mul, transitionMap_comp_eval_apply, transitionMap_map_one
|