AdicCompletion

📁 Source: Mathlib/RingTheory/Smooth/AdicCompletion.lean

Statistics

Metric	Count
Definitions AdicCompletion	1
Theorems exists_adicCompletionEvalOneₐ_comp_eq, exists_kerProj_comp_eq_id, exists_mkₐ_comp_eq_of_isAdicComplete	3
Total	4

Algebra.FormallySmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_adicCompletionEvalOneₐ_comp_eq 📖	mathematical	—	AlgHom.comp AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 AdicCompletion.instCommRing Ideal.Quotient.semiring AdicCompletion.instAlgebra Ideal.instAlgebraQuotient AlgHom.restrictScalars Algebra.id AdicCompletion.instIsScalarTower Algebra.toSMul IsScalarTower.right Ideal.Quotient.isScalarTower AdicCompletion.evalOneₐ	—	AdicCompletion.instIsScalarTower IsScalarTower.right Ideal.Quotient.isScalarTower AlgHom.ext Ideal.instIsTwoSided_1 AdicCompletion.evalOneₐ_liftAlgHom le_of_eq LE.le.trans Ideal.Quotient.factor_comp_apply Ideal.Quotient.factor_eq
exists_kerProj_comp_eq_id 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	AlgHom.comp AdicCompletion RingHom.ker AlgHomClass.toRingHomClass AlgHom.algHomClass Ring.toAddCommGroup CommRing.toRing Semiring.toModule AdicCompletion.instCommRing AdicCompletion.instAlgebra AdicCompletion.kerProj AlgHom.id	—	AlgHomClass.toRingHomClass AlgHom.algHomClass AdicCompletion.instIsScalarTower IsScalarTower.right Ideal.Quotient.isScalarTower RingHom.instIsTwoSidedKer exists_adicCompletionEvalOneₐ_comp_eq AlgHom.ext AlgEquiv.apply_symm_apply
exists_mkₐ_comp_eq_of_isAdicComplete 📖	mathematical	—	AlgHom.comp HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient CommRing.toCommSemiring CommSemiring.toSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 Ideal.Quotient.algebra Ideal.Quotient.mkₐ	—	AdicCompletion.instIsScalarTower IsScalarTower.right Ideal.Quotient.isScalarTower Ideal.instIsTwoSided_1 exists_adicCompletionEvalOneₐ_comp_eq AlgHom.ext AdicCompletion.mk_ofAlgEquiv_symm_eq_evalOneₐ

(root)

Definitions

Name	Category	Theorems
AdicCompletion 📖	CompOp	113 math math: AdicCompletion.of_surjective_iff, AdicCompletion.val_sub_apply, AdicCompletion.mk_zero_of, AdicCompletion.map_val_apply, AdicCompletion.of_ofAlgEquiv_symm, AdicCompletion.instIsScalarTower_1, AdicCompletion.val_smul, AdicCompletion.incl_apply, AdicCompletion.map_ext'_iff, AdicCompletion.ofTensorProduct_surjective_of_finite, AdicCompletion.val_smul_eq_evalₐ_smul, AdicCompletion.pi_apply_coe, AdicCompletion.map_injective, AdicCompletion.val_add_apply, AdicCompletion.smul_eval, AdicCompletion.factor_eval_eq_evalₐ, IsAdicComplete.of_liftRingHom, AdicCompletion.instIsCentralScalar, AdicCompletion.sumInv_apply, AdicCompletion.sum_lof, AdicCompletion.mkₐ_apply_coe, AdicCompletion.map_comp_apply, AdicCompletion.val_sum, IsAdicComplete.of_lift, AdicCompletion.map_comp, AdicCompletion.range_eval, AdicCompletion.val_neg_apply, AdicCompletion.transitionMap_comp_eval, AdicCompletion.map_id, AdicCompletion.instIsHausdorff, AdicCompletion.sumInv_comp_sum, AdicCompletion.coe_eval, AdicCompletion.coe_ofTensorProductEquivOfFiniteNoetherian, AdicCompletion.factorₐ_evalₐ_one, AdicCompletion.val_mul, AdicCompletion.ofTensorProductEquivOfFiniteNoetherian_symm_of, AdicCompletion.mk_ofAlgEquiv_symm, AdicCompletion.ofTensorProduct_bijective_of_finite_of_isNoetherian, AdicCompletion.kerProj_surjective, AdicCompletion.of_bijective_iff, IsAdicComplete.of_comp_lift, AdicCompletion.ofTensorProduct_bijective_of_pi_of_fintype, AdicCompletion.map_mk, AdicCompletion.ofAlgEquiv_apply, AdicCompletion.of_surjective, IsAdicComplete.ofAlgEquiv_comp_liftRingHom, AdicCompletion.sum_of, AdicCompletion.mk_surjective, AdicCompletion.map_ext''_iff, AdicCompletion.congr_symm_apply, AdicCompletion.of_ofLinearEquiv_symm, AdicCompletion.kerProj_of, AdicCompletion.evalOneₐ_of, IsAdicComplete.StrictMono.of_comp_lift, AdicCompletion.val_add, AdicCompletion.mk_smul_top_ofAlgEquiv_symm, AdicCompletion.val_one, AdicCompletion.tensor_map_id_left_eq_map, AdicCompletion.factor_eval_liftRingHom, AdicCompletion.of_inj, AdicCompletion.ofTensorProduct_tmul, AdicCompletion.map_exact, AdicCompletion.evalₐ_liftAlgHom, AdicCompletion.surjective_evalₐ, AdicCompletion.mk_ofAlgEquiv_symm_eq_evalOneₐ, AdicCompletion.of_injective, AdicCompletion.val_sub, AdicCompletion.val_neg, AdicCompletion.ofTensorProductEquivOfFiniteNoetherian_apply, AdicCompletion.sumEquivOfFintype_apply, AdicCompletion.of_bijective, Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq, AdicCompletion.evalₐ_of, AdicCompletion.evalOneₐ_surjective, AdicCompletion.factor_evalₐ_eq_eval, AdicCompletion.evalₐ_comp_liftRingHom, AdicCompletion.eval_of, AdicCompletion.map_zero, AdicCompletion.component_sumInv, AdicCompletion.evalₐ_mk, AdicCompletion.piEquivOfFintype_apply, IsAdicComplete.StrictMono.of_lift, AdicCompletion.evalₐ_mkₐ, AdicCompletion.ofTensorProduct_naturality, AdicCompletion.val_zero, AdicCompletion.instIsScalarTower, AdicCompletion.ofLinearEquiv_apply, AdicCompletion.mk_apply_coe, AdicCompletion.congr_apply, Algebra.FormallySmooth.exists_kerProj_comp_eq_id, AdicCompletion.of_injective_iff, AdicCompletion.eval_lift_apply, AdicCompletion.val_zero_apply, AdicCompletion.tensor_map_id_left_injective_of_injective, AdicCompletion.eval_surjective, AdicCompletion.instSMulCommClass, AdicCompletion.sumEquivOfFintype_symm_apply, AdicCompletion.eval_apply, AdicCompletion.flat_of_isNoetherian, AdicCompletion.piEquivFin_apply, AdicCompletion.ofLinearEquiv_symm_of, AdicCompletion.val_sum_apply, AdicCompletion.evalOneₐ_liftAlgHom, AdicCompletion.evalₐ_liftRingHom, AdicCompletion.map_of, AdicCompletion.map_surjective_of_mkQ_comp_surjective, AdicCompletion.of_apply, AdicCompletion.map_surjective, AdicCompletion.eval_comp_of, AdicCompletion.sum_comp_sumInv, AdicCompletion.val_smul_apply, AdicCompletion.eval_lift, AdicCompletion.ofAlgEquiv_symm_of

---

← Back to Index