Algebra

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

Statistics

Metric	Count
Definitions subalgebra, subring, evalOneₐ, evalₐ, instAlgebra, instAlgebraAdicCauchySequence, instCommRing, instCommRingAdicCauchySequence, instIntCast, instIntCastAdicCauchySequence, instModuleQuotientIdealHSMulTopSubmodule, instMul, instMulAdicCauchySequence, instNatCast, instNatCastAdicCauchySequence, instOne, instOneAdicCauchySequence, instPowAdicCauchySequenceNat, instPowNat, instSMulQuotientIdealHSMulTopSubmodule, kerProj, liftAlgHom, liftRingHom, mkₐ, ofAlgEquiv, smul, subalgebra, subring, transitionMapₐ	29
Theorems mk_eq_mk, evalOneₐ_liftAlgHom, evalOneₐ_of, evalOneₐ_surjective, evalₐ_comp_liftRingHom, evalₐ_liftAlgHom, evalₐ_liftRingHom, evalₐ_mk, evalₐ_mkₐ, evalₐ_of, ext_evalₐ, factor_eval_eq_evalₐ, factor_eval_liftRingHom, factor_evalₐ_eq_eval, factorₐ_evalₐ_one, instIsScalarTowerQuotientIdealHSMulTopSubmodule, instIsScalarTower_1, kerProj_of, kerProj_surjective, mk_ofAlgEquiv_symm, mk_ofAlgEquiv_symm_eq_evalOneₐ, mk_smul_mk, mk_smul_top_ofAlgEquiv_symm, mkₐ_apply_coe, mul_apply, ofAlgEquiv_apply, ofAlgEquiv_symm_of, of_ofAlgEquiv_symm, one_apply, smul_eval, smul_mk, surjective_evalₐ, transitionMap_ideal_mk, transitionMap_map_mul, transitionMap_map_one, transitionMap_map_pow, val_mul, val_one, val_smul_eq_evalₐ_smul	39
Total	68

AdicCompletion

Definitions

Name	Category	Theorems
evalOneₐ 📖	CompOp	6 math math: factorₐ_evalₐ_one, evalOneₐ_of, mk_ofAlgEquiv_symm_eq_evalOneₐ, Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq, evalOneₐ_surjective, evalOneₐ_liftAlgHom
evalₐ 📖	CompOp	12 math math: val_smul_eq_evalₐ_smul, factor_eval_eq_evalₐ, factorₐ_evalₐ_one, mk_ofAlgEquiv_symm, evalₐ_liftAlgHom, surjective_evalₐ, evalₐ_of, factor_evalₐ_eq_eval, evalₐ_comp_liftRingHom, evalₐ_mk, evalₐ_mkₐ, evalₐ_liftRingHom
instAlgebra 📖	CompOp	36 math math: of_ofAlgEquiv_symm, ofTensorProduct_surjective_of_finite, val_smul_eq_evalₐ_smul, factor_eval_eq_evalₐ, mkₐ_apply_coe, coe_ofTensorProductEquivOfFiniteNoetherian, factorₐ_evalₐ_one, ofTensorProductEquivOfFiniteNoetherian_symm_of, mk_ofAlgEquiv_symm, ofTensorProduct_bijective_of_finite_of_isNoetherian, kerProj_surjective, ofTensorProduct_bijective_of_pi_of_fintype, ofAlgEquiv_apply, IsAdicComplete.ofAlgEquiv_comp_liftRingHom, kerProj_of, evalOneₐ_of, mk_smul_top_ofAlgEquiv_symm, tensor_map_id_left_eq_map, ofTensorProduct_tmul, evalₐ_liftAlgHom, surjective_evalₐ, mk_ofAlgEquiv_symm_eq_evalOneₐ, ofTensorProductEquivOfFiniteNoetherian_apply, Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq, evalₐ_of, evalOneₐ_surjective, factor_evalₐ_eq_eval, evalₐ_comp_liftRingHom, evalₐ_mk, evalₐ_mkₐ, ofTensorProduct_naturality, Algebra.FormallySmooth.exists_kerProj_comp_eq_id, tensor_map_id_left_injective_of_injective, evalOneₐ_liftAlgHom, evalₐ_liftRingHom, ofAlgEquiv_symm_of
instAlgebraAdicCauchySequence 📖	CompOp	2 math math: mkₐ_apply_coe, evalₐ_mkₐ
instCommRing 📖	CompOp	64 math math: map_val_apply, of_ofAlgEquiv_symm, map_ext'_iff, ofTensorProduct_surjective_of_finite, val_smul_eq_evalₐ_smul, pi_apply_coe, map_injective, factor_eval_eq_evalₐ, IsAdicComplete.of_liftRingHom, sumInv_apply, sum_lof, mkₐ_apply_coe, map_comp_apply, map_comp, map_id, sumInv_comp_sum, coe_ofTensorProductEquivOfFiniteNoetherian, factorₐ_evalₐ_one, ofTensorProductEquivOfFiniteNoetherian_symm_of, mk_ofAlgEquiv_symm, ofTensorProduct_bijective_of_finite_of_isNoetherian, kerProj_surjective, ofTensorProduct_bijective_of_pi_of_fintype, map_mk, ofAlgEquiv_apply, IsAdicComplete.ofAlgEquiv_comp_liftRingHom, sum_of, congr_symm_apply, kerProj_of, evalOneₐ_of, mk_smul_top_ofAlgEquiv_symm, tensor_map_id_left_eq_map, factor_eval_liftRingHom, ofTensorProduct_tmul, map_exact, evalₐ_liftAlgHom, surjective_evalₐ, mk_ofAlgEquiv_symm_eq_evalOneₐ, ofTensorProductEquivOfFiniteNoetherian_apply, sumEquivOfFintype_apply, Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq, evalₐ_of, evalOneₐ_surjective, factor_evalₐ_eq_eval, evalₐ_comp_liftRingHom, map_zero, component_sumInv, evalₐ_mk, piEquivOfFintype_apply, evalₐ_mkₐ, ofTensorProduct_naturality, congr_apply, Algebra.FormallySmooth.exists_kerProj_comp_eq_id, tensor_map_id_left_injective_of_injective, sumEquivOfFintype_symm_apply, flat_of_isNoetherian, piEquivFin_apply, evalOneₐ_liftAlgHom, evalₐ_liftRingHom, map_of, map_surjective_of_mkQ_comp_surjective, map_surjective, sum_comp_sumInv, ofAlgEquiv_symm_of
instCommRingAdicCauchySequence 📖	CompOp	2 math math: mkₐ_apply_coe, evalₐ_mkₐ
instIntCast 📖	CompOp	—
instIntCastAdicCauchySequence 📖	CompOp	—
instModuleQuotientIdealHSMulTopSubmodule 📖	CompOp	—
instMul 📖	CompOp	1 math math: val_mul
instMulAdicCauchySequence 📖	CompOp	1 math math: mul_apply
instNatCast 📖	CompOp	—
instNatCastAdicCauchySequence 📖	CompOp	—
instOne 📖	CompOp	2 math math: ofTensorProductEquivOfFiniteNoetherian_symm_of, val_one
instOneAdicCauchySequence 📖	CompOp	1 math math: one_apply
instPowAdicCauchySequenceNat 📖	CompOp	—
instPowNat 📖	CompOp	—
instSMulQuotientIdealHSMulTopSubmodule 📖	CompOp	4 math math: val_smul_eq_evalₐ_smul, smul_eval, mk_smul_mk, instIsScalarTowerQuotientIdealHSMulTopSubmodule
kerProj 📖	CompOp	3 math math: kerProj_surjective, kerProj_of, Algebra.FormallySmooth.exists_kerProj_comp_eq_id
liftAlgHom 📖	CompOp	2 math math: evalₐ_liftAlgHom, evalOneₐ_liftAlgHom
liftRingHom 📖	CompOp	5 math math: IsAdicComplete.of_liftRingHom, IsAdicComplete.ofAlgEquiv_comp_liftRingHom, factor_eval_liftRingHom, evalₐ_comp_liftRingHom, evalₐ_liftRingHom
mkₐ 📖	CompOp	2 math math: mkₐ_apply_coe, evalₐ_mkₐ
ofAlgEquiv 📖	CompOp	7 math math: of_ofAlgEquiv_symm, mk_ofAlgEquiv_symm, ofAlgEquiv_apply, IsAdicComplete.ofAlgEquiv_comp_liftRingHom, mk_smul_top_ofAlgEquiv_symm, mk_ofAlgEquiv_symm_eq_evalOneₐ, ofAlgEquiv_symm_of
smul 📖	CompOp	3 math math: instIsScalarTower_1, smul_eval, ofTensorProduct_tmul
subalgebra 📖	CompOp	—
subring 📖	CompOp	—
transitionMapₐ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evalOneₐ_liftAlgHom 📖	mathematical	AlgHom.comp HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Submodule.instPowNat Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction CommRing.toCommSemiring CommSemiring.toSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 IsScalarTower.right Algebra.id Ideal.Quotient.algebra Ideal.Quotient.factorₐ Ideal.pow_le_pow_right	DFunLike.coe AlgHom AdicCompletion Ring.toAddCommGroup Ideal.instHasQuotient_1 instCommRing Ideal.Quotient.semiring instAlgebra Ideal.instAlgebraQuotient AlgHom.funLike evalOneₐ liftAlgHom	—	IsScalarTower.right IsScalarTower.left Ideal.instIsTwoSided_1 Ideal.pow_le_pow_right evalₐ_liftAlgHom
evalOneₐ_of 📖	mathematical	—	DFunLike.coe AlgHom AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 instCommRing Ideal.Quotient.semiring instAlgebra Algebra.id Ideal.instAlgebraQuotient AlgHom.funLike evalOneₐ LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModuleOfIsScalarTower Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike of RingHom Ring.toSemiring Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike	—	IsScalarTower.left
evalOneₐ_surjective 📖	mathematical	—	AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 DFunLike.coe AlgHom instCommRing Ideal.Quotient.semiring instAlgebra Algebra.id Ideal.instAlgebraQuotient AlgHom.funLike evalOneₐ	—	Ideal.instIsTwoSided_1 pow_one Ideal.Quotient.factor_surjective surjective_evalₐ
evalₐ_comp_liftRingHom 📖	mathematical	RingHom.comp HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Submodule.instPowNat Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Module.toDistribMulAction Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.IsTwoSided.instHPowNat Ideal.instIsTwoSided_1 Ideal.Quotient.factorPow	AdicCompletion Ring.toAddCommGroup CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 IsScalarTower.right Algebra.id instCommRing Ideal.Quotient.semiring RingHomClass.toRingHom AlgHom instAlgebra Ideal.instAlgebraQuotient AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass evalₐ liftRingHom	—	IsScalarTower.right IsScalarTower.left Ideal.IsTwoSided.instHPowNat Ideal.instIsTwoSided_1 RingHom.ext AlgHomClass.toRingHomClass AlgHom.algHomClass evalₐ_liftRingHom
evalₐ_liftAlgHom 📖	mathematical	AlgHom.comp HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Submodule.instPowNat Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction CommRing.toCommSemiring CommSemiring.toSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 IsScalarTower.right Algebra.id Ideal.Quotient.algebra Ideal.Quotient.factorₐ Ideal.pow_le_pow_right	DFunLike.coe AlgHom AdicCompletion Ring.toAddCommGroup Ideal.instHasQuotient_1 instCommRing Ideal.Quotient.semiring instAlgebra Ideal.instAlgebraQuotient AlgHom.funLike evalₐ liftAlgHom	—	IsScalarTower.right IsScalarTower.left Ideal.instIsTwoSided_1 Ideal.pow_le_pow_right evalₐ_liftRingHom RingHom.ext Ideal.IsTwoSided.instHPowNat
evalₐ_liftRingHom 📖	mathematical	RingHom.comp HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Submodule.instPowNat Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Module.toDistribMulAction Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.IsTwoSided.instHPowNat Ideal.instIsTwoSided_1 Ideal.Quotient.factorPow	DFunLike.coe AlgHom AdicCompletion Ring.toAddCommGroup CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 IsScalarTower.right Algebra.id instCommRing Ideal.Quotient.semiring instAlgebra Ideal.instAlgebraQuotient AlgHom.funLike evalₐ RingHom RingHom.instFunLike liftRingHom	—	IsScalarTower.right IsScalarTower.left Ideal.IsTwoSided.instHPowNat Ideal.instIsTwoSided_1 le_of_eq Ideal.mul_top factor_eval_eq_evalₐ LE.le.trans Ideal.Quotient.factor_comp_apply Ideal.Quotient.factor_eq
evalₐ_mk 📖	mathematical	—	DFunLike.coe AlgHom AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Submodule.instPowNat IsScalarTower.right Algebra.id instCommRing Ideal.Quotient.semiring instAlgebra Ideal.instAlgebraQuotient AlgHom.funLike evalₐ LinearMap RingHom.id Semiring.toNonAssocSemiring AdicCauchySequence AddCommGroup.toAddCommMonoid AdicCauchySequence.instAddCommGroup instAddCommGroup AdicCauchySequence.instModule instModuleOfIsScalarTower Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike RingHom Ring.toSemiring Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike IsAdicCauchy	—	IsScalarTower.right
evalₐ_mkₐ 📖	mathematical	—	DFunLike.coe AlgHom AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Submodule.instPowNat IsScalarTower.right Algebra.id instCommRing Ideal.Quotient.semiring instAlgebra Ideal.instAlgebraQuotient AlgHom.funLike evalₐ AdicCauchySequence instCommRingAdicCauchySequence instAlgebraAdicCauchySequence mkₐ RingHom Ring.toSemiring Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike IsAdicCauchy	—	IsScalarTower.right Ideal.instIsTwoSided_1
evalₐ_of 📖	mathematical	—	DFunLike.coe AlgHom AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Submodule.instPowNat IsScalarTower.right Algebra.id instCommRing Ideal.Quotient.semiring instAlgebra Ideal.instAlgebraQuotient AlgHom.funLike evalₐ LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModuleOfIsScalarTower Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike of RingHom Ring.toSemiring Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike	—	IsScalarTower.right
ext_evalₐ 📖	—	DFunLike.coe AlgHom AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Submodule.instPowNat IsScalarTower.right Algebra.id instCommRing Ideal.Quotient.semiring instAlgebra Ideal.instAlgebraQuotient AlgHom.funLike evalₐ	—	—	IsScalarTower.right ext Ideal.ext IsScalarTower.left Ideal.smul_top_eq_map Submodule.restrictScalars.congr_simp Ideal.map_id Submodule.restrictScalars_self AlgEquiv.injective Ideal.instIsTwoSided_1
factor_eval_eq_evalₐ 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instSMul IsScalarTower.right Algebra.id Submodule.instPowNat Top.top Submodule.instTop	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Ring.toAddCommGroup Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike Submodule.factor AdicCompletion IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction instAddCommGroup instModuleOfIsScalarTower Algebra.toSMul eval AlgHom Ideal.instHasQuotient_1 instCommRing Ideal.Quotient.semiring instAlgebra Ideal.instAlgebraQuotient AlgHom.funLike evalₐ	—	IsScalarTower.right Ideal.instIsTwoSided_1
factor_eval_liftRingHom 📖	mathematical	RingHom.comp HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Submodule.instPowNat Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Module.toDistribMulAction Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.IsTwoSided.instHPowNat Ideal.instIsTwoSided_1 Ideal.Quotient.factorPow CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.instSMul IsScalarTower.right Algebra.id Top.top Submodule.instTop	DFunLike.coe LinearMap RingHom.id Submodule AddCommGroup.toAddCommMonoid Ring.toAddCommGroup Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike Submodule.factor AdicCompletion instAddCommGroup instModuleOfIsScalarTower Algebra.toSMul eval RingHom instCommRing RingHom.instFunLike liftRingHom Ideal.instHasQuotient_1 Ideal.Quotient.semiring	—	IsScalarTower.right IsScalarTower.left Ideal.IsTwoSided.instHPowNat Ideal.instIsTwoSided_1 LE.le.trans Ideal.Quotient.factor_comp_apply Ideal.Quotient.factor_eq
factor_evalₐ_eq_eval 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id Submodule.instSMul Top.top Submodule.instTop	DFunLike.coe RingHom HasQuotient.Quotient Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Ideal.Quotient.factor AlgHom AdicCompletion Ring.toAddCommGroup Ideal.instHasQuotient_1 instCommRing Ideal.Quotient.semiring instAlgebra Ideal.instAlgebraQuotient AlgHom.funLike evalₐ LinearMap RingHom.id Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction instAddCommGroup Submodule.Quotient.addCommGroup instModuleOfIsScalarTower Algebra.toSMul Submodule.Quotient.module LinearMap.instFunLike eval	—	IsScalarTower.right Ideal.instIsTwoSided_1 IsScalarTower.left le_of_eq LE.le.trans Ideal.Quotient.factor_comp_apply Ideal.Quotient.factor_eq
factorₐ_evalₐ_one 📖	mathematical	—	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Ideal.Quotient.factor AlgHom AdicCompletion Ring.toAddCommGroup Semiring.toModule Ideal.instHasQuotient_1 Submodule.instPowNat IsScalarTower.right instCommRing Ideal.Quotient.semiring instAlgebra Ideal.instAlgebraQuotient AlgHom.funLike evalₐ evalOneₐ	—	Ideal.instIsTwoSided_1 IsScalarTower.right
instIsScalarTowerQuotientIdealHSMulTopSubmodule 📖	mathematical	—	IsScalarTower HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Submodule.instSMul Semiring.toModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsScalarTower.right Algebra.id Top.top Submodule.instTop Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.Quotient.instSMul Ring.toAddCommGroup instSMulQuotientIdealHSMulTopSubmodule	—	IsScalarTower.right IsScalarTower.left Quotient.inductionOn' Submodule.Quotient.mk_smul Ideal.instIsTwoSided_1 smul_assoc Submodule.Quotient.isScalarTower
instIsScalarTower_1 📖	mathematical	—	IsScalarTower AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instSMul Algebra.toSMul Algebra.id IsScalarTower.right smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid	—	IsScalarTower.right IsScalarTower.left ext smul_eval val_smul_apply smul_assoc instIsScalarTowerQuotientIdealHSMulTopSubmodule
kerProj_of 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	AdicCompletion RingHom.ker AlgHomClass.toRingHomClass AlgHom.algHomClass Ring.toAddCommGroup CommRing.toRing Semiring.toModule instCommRing instAlgebra kerProj LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModuleOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike of	—	AlgHomClass.toRingHomClass AlgHom.algHomClass IsScalarTower.left
kerProj_surjective 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	AdicCompletion RingHom.ker AlgHomClass.toRingHomClass AlgHom.algHomClass Ring.toAddCommGroup CommRing.toRing Semiring.toModule instCommRing instAlgebra kerProj	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.instIsTwoSidedKer AlgEquiv.surjective evalOneₐ_surjective
mk_ofAlgEquiv_symm 📖	mathematical	—	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instPowNat Semiring.toModule IsScalarTower.right Algebra.id Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike AlgEquiv AdicCompletion Ring.toAddCommGroup instCommRing instAlgebra AlgEquiv.instFunLike AlgEquiv.symm ofAlgEquiv AlgHom Ideal.instHasQuotient_1 Ideal.Quotient.semiring Ideal.instAlgebraQuotient AlgHom.funLike evalₐ	—	IsScalarTower.right Ideal.instIsTwoSided_1 IsScalarTower.left mk_smul_top_ofAlgEquiv_symm
mk_ofAlgEquiv_symm_eq_evalOneₐ 📖	mathematical	—	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike AlgEquiv AdicCompletion Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing instAlgebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm ofAlgEquiv AlgHom Ideal.instHasQuotient_1 Ideal.Quotient.semiring Ideal.instAlgebraQuotient AlgHom.funLike evalOneₐ	—	Ideal.instIsTwoSided_1 IsScalarTower.right
mk_smul_mk 📖	mathematical	—	HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instSMul Semiring.toModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsScalarTower.right Algebra.id Top.top Submodule.instTop Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction instSMulQuotientIdealHSMulTopSubmodule DFunLike.coe RingHom Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Submodule.Quotient.instSMul	—	IsScalarTower.left IsScalarTower.right Ideal.instIsTwoSided_1
mk_smul_top_ofAlgEquiv_symm 📖	mathematical	—	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instSMul Semiring.toModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsScalarTower.right Algebra.id Submodule.instPowNat Top.top Submodule.instTop Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike AlgEquiv AdicCompletion Ring.toAddCommGroup instCommRing instAlgebra AlgEquiv.instFunLike AlgEquiv.symm ofAlgEquiv LinearMap RingHom.id Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction instAddCommGroup Submodule.Quotient.addCommGroup instModuleOfIsScalarTower Algebra.toSMul Submodule.Quotient.module LinearMap.instFunLike eval	—	IsScalarTower.right Ideal.instIsTwoSided_1 IsScalarTower.left of_ofAlgEquiv_symm
mkₐ_apply_coe 📖	mathematical	—	DFunLike.coe AlgHom AdicCauchySequence Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AdicCompletion instCommRingAdicCauchySequence instCommRing instAlgebraAdicCauchySequence instAlgebra Algebra.id AlgHom.funLike mkₐ RingHom HasQuotient.Quotient Ideal Ring.toSemiring Ideal.instHasQuotient Submodule AddCommGroup.toAddCommMonoid Submodule.instSMul Submodule.instPowNat Top.top Submodule.instTop Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike IsAdicCauchy	—	—
mul_apply 📖	mathematical	—	IsAdicCauchy Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AdicCauchySequence instMulAdicCauchySequence Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
ofAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Algebra.id instAlgebra AlgEquiv.instFunLike ofAlgEquiv LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModuleOfIsScalarTower Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike of	—	—
ofAlgEquiv_symm_of 📖	mathematical	—	DFunLike.coe AlgEquiv AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing instAlgebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm ofAlgEquiv LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModuleOfIsScalarTower Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike of	—	IsScalarTower.left ofLinearEquiv_symm_of
of_ofAlgEquiv_symm 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule AddCommGroup.toAddCommMonoid instAddCommGroup instModuleOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike of AlgEquiv instCommRing instAlgebra AlgEquiv.instFunLike AlgEquiv.symm ofAlgEquiv	—	IsScalarTower.left of_ofLinearEquiv_symm
one_apply 📖	mathematical	—	IsAdicCauchy Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AdicCauchySequence instOneAdicCauchySequence AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
smul_eval 📖	mathematical	—	AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring smul HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient Ideal Submodule.instSMul Submodule.instPowNat Top.top Submodule.instTop instSMulQuotientIdealHSMulTopSubmodule	—	—
smul_mk 📖	mathematical	—	HasQuotient.Quotient Submodule Ring.toSemiring CommRing.toRing AddCommGroup.toAddCommMonoid Submodule.hasQuotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat IsScalarTower.right Algebra.id Top.top Submodule.instTop Submodule.Quotient.instSMul IsAdicCauchy Ring.toAddCommGroup	—	IsScalarTower.left IsScalarTower.right Submodule.Quotient.mk_smul Ideal.instIsTwoSided_1
surjective_evalₐ 📖	mathematical	—	AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Submodule.instPowNat IsScalarTower.right Algebra.id DFunLike.coe AlgHom instCommRing Ideal.Quotient.semiring instAlgebra Ideal.instAlgebraQuotient AlgHom.funLike evalₐ	—	IsScalarTower.right le_of_eq Submodule.factor_surjective Ideal.mul_le_right Ideal.instIsTwoSided_1 eval_surjective
transitionMap_ideal_mk 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Submodule.hasQuotient Ideal Submodule.instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Top.top Submodule.instTop Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike transitionMap RingHom Ideal.instHasQuotient NonAssocSemiring.toNonUnitalNonAssocSemiring IsScalarTower.right Algebra.id Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike	—	IsScalarTower.left IsScalarTower.right Ideal.instIsTwoSided_1
transitionMap_map_mul 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Submodule.hasQuotient Ideal Submodule.instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Top.top Submodule.instTop Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike transitionMap Ideal.instHasQuotient_1 NonAssocSemiring.toNonUnitalNonAssocSemiring IsScalarTower.right Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing	—	IsScalarTower.right Quotient.inductionOn₂' IsScalarTower.left
transitionMap_map_one 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Submodule.hasQuotient Ideal Submodule.instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Top.top Submodule.instTop Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike transitionMap Ideal.Quotient.one	—	IsScalarTower.left
transitionMap_map_pow 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Submodule.hasQuotient Ideal Submodule.instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Top.top Submodule.instTop Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike transitionMap Ideal.instHasQuotient_1 NonAssocSemiring.toNonUnitalNonAssocSemiring IsScalarTower.right Algebra.id Monoid.toNatPow Ideal.Quotient.semiring	—	IsScalarTower.right Quotient.inductionOn' IsScalarTower.left
val_mul 📖	mathematical	—	AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instMul HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient Ideal Submodule.instSMul Submodule.instPowNat Top.top Submodule.instTop Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing	—	—
val_one 📖	mathematical	—	AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instOne HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient Ideal Submodule.instSMul Submodule.instPowNat Top.top Submodule.instTop Ideal.Quotient.one	—	—
val_smul_eq_evalₐ_smul 📖	mathematical	—	HasQuotient.Quotient Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ring.toAddCommGroup CommRing.toRing Semiring.toModule Submodule.hasQuotient Ideal Submodule.instSMul Submodule.instPowNat Top.top Submodule.instTop IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.right Algebra.id instSMulQuotientIdealHSMulTopSubmodule Ideal.instHasQuotient_1 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Submodule.Quotient.addCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Ideal.Quotient.semiring Module.instQuotientIdealSubmoduleHSMulTop Ideal.instIsTwoSided_1 DFunLike.coe AlgHom AdicCompletion instCommRing instAlgebra Ideal.instAlgebraQuotient AlgHom.funLike evalₐ	—	IsScalarTower.left IsScalarTower.right induction_on Ideal.instIsTwoSided_1 Quotient.inductionOn'

AdicCompletion.AdicCauchySequence

Definitions

Name	Category	Theorems
subalgebra 📖	CompOp	—
subring 📖	CompOp	—

AdicCompletion.Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_eq_mk 📖	mathematical	—	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instPowNat Semiring.toModule IsScalarTower.right Algebra.id Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike AdicCompletion.IsAdicCauchy Ring.toAddCommGroup	—	IsScalarTower.right IsScalarTower.left Ideal.smul_top_eq_map Submodule.restrictScalars.congr_simp Ideal.map_id Submodule.restrictScalars_self Ideal.instIsTwoSided_1 SModEq.symm

---

← Back to Index