Functoriality

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

Statistics

Metric	Count
Definitions map, map, pi, piEquivFin, piEquivOfFintype, sum, sumEquivOfFintype, sumInv, reduceModIdeal	9
Theorems map_apply_coe, map_comp, map_comp_apply, map_id, map_zero, component_sumInv, congr_apply, congr_symm_apply, exists_smodEq_pow_add_one_smul, exists_smodEq_pow_smul_top_and_mkQ_eq, exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top, map_comp, map_comp_apply, map_ext, map_ext', map_ext'', map_ext''_iff, map_ext'_iff, map_id, map_mk, map_of, map_surjective_of_mkQ_comp_surjective, map_val_apply, map_zero, piEquivFin_apply, piEquivOfFintype_apply, pi_apply_coe, sumEquivOfFintype_apply, sumEquivOfFintype_symm_apply, sumInv_apply, sumInv_comp_sum, sum_comp_sumInv, sum_lof, sum_of, transitionMap_comp_reduceModIdeal, reduceModIdeal_apply, surjective_of_mkQ_comp_surjective, surjective_of_mk_map_comp_surjective	38
Total	47

AdicCompletion

Definitions

Name	Category	Theorems
map 📖	CompOp	19 math math: map_val_apply, map_injective, sumInv_apply, sum_lof, map_comp_apply, map_comp, map_id, map_mk, sum_of, congr_symm_apply, tensor_map_id_left_eq_map, map_exact, map_zero, component_sumInv, ofTensorProduct_naturality, congr_apply, map_of, map_surjective_of_mkQ_comp_surjective, map_surjective
pi 📖	CompOp	3 math math: pi_apply_coe, piEquivOfFintype_apply, piEquivFin_apply
piEquivFin 📖	CompOp	1 math math: piEquivFin_apply
piEquivOfFintype 📖	CompOp	1 math math: piEquivOfFintype_apply
sum 📖	CompOp	5 math math: sum_lof, sumInv_comp_sum, sum_of, sumEquivOfFintype_apply, sum_comp_sumInv
sumEquivOfFintype 📖	CompOp	2 math math: sumEquivOfFintype_apply, sumEquivOfFintype_symm_apply
sumInv 📖	CompOp	5 math math: sumInv_apply, sumInv_comp_sum, component_sumInv, sumEquivOfFintype_symm_apply, sum_comp_sumInv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
component_sumInv 📖	mathematical	—	DFunLike.coe LinearMap AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring DirectSum AddCommGroup.toAddCommMonoid instAddCommGroup instAddCommMonoidDirectSum DirectSum.instModule module LinearMap.instFunLike DirectSum.component DirectSum.instAddCommGroup sumInv map	—	induction_on IsScalarTower.left
congr_apply 📖	mathematical	—	DFunLike.coe LinearEquiv AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid instAddCommGroup module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv congr LinearMap LinearMap.instFunLike map LinearEquiv.toLinearMap	—	RingHomInvPair.ids
congr_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid instAddCommGroup module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm congr LinearMap LinearMap.instFunLike map LinearEquiv.toLinearMap	—	RingHomInvPair.ids
exists_smodEq_pow_add_one_smul 📖	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 Top.top Submodule.instTop DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike LinearMap.comp RingHomCompTriple.ids Submodule.mkQ SetLike.instMembership Submodule.setLike Submodule.instPowNat IsScalarTower.right Algebra.id	SModEq	—	IsScalarTower.left RingHomCompTriple.ids IsScalarTower.right Submodule.smul_induction_on' Submodule.smul_mem_smul Submodule.mem_top map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass pow_succ smul_smul SModEq.smul' AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass map_add SemilinearMapClass.toAddHomClass SModEq.add
exists_smodEq_pow_smul_top_and_mkQ_eq 📖	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 Top.top Submodule.instTop DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike LinearMap.comp RingHomCompTriple.ids Submodule.mkQ Submodule.instPowNat NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Submodule.factor Submodule.pow_smul_top_le IsScalarTower.right Algebra.id	SModEq	—	IsScalarTower.left RingHomCompTriple.ids IsScalarTower.right Submodule.pow_smul_top_le Submodule.mkQ_surjective SModEq.eq_1 Submodule.mkQ_apply exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top
exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top 📖	—	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 Top.top Submodule.instTop DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike LinearMap.comp RingHomCompTriple.ids Submodule.mkQ SModEq Submodule.instPowNat IsScalarTower.right Algebra.id	—	—	IsScalarTower.left RingHomCompTriple.ids IsScalarTower.right exists_smodEq_pow_add_one_smul SModEq.sub_mem SModEq.symm sub_add_cancel_left AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass sub_sub_eq_add_sub add_comm
map_comp 📖	mathematical	—	LinearMap.comp AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing AddCommGroup.toAddCommMonoid instAddCommGroup module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids map	—	map_ext' RingHomCompTriple.ids ext IsScalarTower.left IsScalarTower.right
map_comp_apply 📖	mathematical	—	DFunLike.coe LinearMap AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup module LinearMap.instFunLike map LinearMap.comp RingHomCompTriple.ids	—	RingHomCompTriple.ids map_comp
map_ext 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AdicCauchySequence AdicCompletion AddCommGroup.toAddCommMonoid AdicCauchySequence.instAddCommGroup instAddCommGroup AdicCauchySequence.instModule instModuleOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike	—	—	IsScalarTower.left induction_on
map_ext' 📖	—	DFunLike.coe LinearMap AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup module LinearMap.instFunLike AdicCauchySequence AdicCauchySequence.instAddCommGroup AdicCauchySequence.instModule instModuleOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	—	IsScalarTower.left LinearMap.ext induction_on
map_ext'' 📖	—	LinearMap.comp AdicCauchySequence AdicCompletion CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AdicCauchySequence.instAddCommGroup instAddCommGroup AdicCauchySequence.instModule instModuleOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—	IsScalarTower.left RingHomCompTriple.ids LinearMap.ext induction_on LinearMap.ext_iff
map_ext''_iff 📖	mathematical	—	LinearMap.comp AdicCauchySequence AdicCompletion CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AdicCauchySequence.instAddCommGroup instAddCommGroup AdicCauchySequence.instModule instModuleOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	IsScalarTower.left RingHomCompTriple.ids map_ext''
map_ext'_iff 📖	mathematical	—	DFunLike.coe LinearMap AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup module LinearMap.instFunLike AdicCauchySequence AdicCauchySequence.instAddCommGroup AdicCauchySequence.instModule instModuleOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	IsScalarTower.left map_ext'
map_id 📖	mathematical	—	map LinearMap.id CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule instCommRing instAddCommGroup module	—	map_ext' ext IsScalarTower.left IsScalarTower.right
map_mk 📖	mathematical	—	DFunLike.coe LinearMap AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup module LinearMap.instFunLike map AdicCauchySequence AdicCauchySequence.instAddCommGroup AdicCauchySequence.instModule instModuleOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AdicCauchySequence.map	—	IsScalarTower.left
map_of 📖	mathematical	—	DFunLike.coe LinearMap AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup module LinearMap.instFunLike map instModuleOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction of	—	IsScalarTower.left
map_surjective_of_mkQ_comp_surjective 📖	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 Top.top Submodule.instTop DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike LinearMap.comp RingHomCompTriple.ids Submodule.mkQ	AdicCompletion Ring.toAddCommGroup instCommRing instAddCommGroup module map	—	IsScalarTower.left RingHomCompTriple.ids IsScalarTower.right Equiv.injective RingHomInvPair.ids RingHomSurjective.ids Submodule.map.congr_simp pow_zero Ideal.one_eq_top Submodule.top_smul Submodule.map_top LinearMap.range_id Unique.instSubsingleton exists_smodEq_pow_smul_top_and_mkQ_eq Submodule.pow_smul_top_le transitionMap_comp_eval_apply IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd Submodule.eq_factor_of_eq_factor_succ ext
map_val_apply 📖	mathematical	—	DFunLike.coe LinearMap AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup module LinearMap.instFunLike map HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Submodule.instPowNat IsScalarTower.right Algebra.id Ideal.Quotient.semiring Submodule Submodule.hasQuotient Submodule.instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop Ring.toSemiring Submodule.Quotient.addCommGroup Module.instQuotientIdealSubmoduleHSMulTop Ideal.instIsTwoSided_1 LinearMap.reduceModIdeal	—	—
map_zero 📖	mathematical	—	map LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instZero AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule instCommRing instAddCommGroup module	—	map_ext' ext IsScalarTower.left map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
piEquivFin_apply 📖	mathematical	—	DFunLike.coe LinearEquiv AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring AddCommGroup.toAddCommMonoid instAddCommGroup Pi.addCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv piEquivFin LinearMap Pi.module LinearMap.instFunLike pi	—	RingHomInvPair.ids piEquivOfFintype_apply
piEquivOfFintype_apply 📖	mathematical	—	DFunLike.coe LinearEquiv AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommGroup Pi.module AddCommGroup.toAddCommMonoid instAddCommGroup Pi.addCommMonoid module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv piEquivOfFintype LinearMap LinearMap.instFunLike pi	—	RingHomInvPair.ids RingHomCompTriple.ids map_comp_apply LinearEquiv.symm_trans_self map_id LinearEquiv.apply_symm_apply
pi_apply_coe 📖	mathematical	—	DFunLike.coe LinearMap AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring Pi.addCommGroup Pi.module AddCommGroup.toAddCommMonoid instAddCommGroup Pi.addCommMonoid module LinearMap.instFunLike pi HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Submodule.instPowNat Ideal.Quotient.semiring Submodule Submodule.hasQuotient Submodule.instSMul Top.top Submodule.instTop Ring.toSemiring Submodule.Quotient.addCommGroup Module.instQuotientIdealSubmoduleHSMulTop LinearMap.reduceModIdeal LinearMap.proj	—	—
sumEquivOfFintype_apply 📖	mathematical	—	DFunLike.coe LinearEquiv AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum AddCommGroup.toAddCommMonoid instAddCommGroup DirectSum.instAddCommGroup DirectSum.instModule instAddCommMonoidDirectSum module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv sumEquivOfFintype LinearMap LinearMap.instFunLike sum	—	RingHomInvPair.ids
sumEquivOfFintype_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum AddCommGroup.toAddCommMonoid DirectSum.instAddCommGroup DirectSum.instModule instAddCommGroup instAddCommMonoidDirectSum module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm sumEquivOfFintype LinearMap LinearMap.instFunLike sumInv	—	RingHomInvPair.ids
sumInv_apply 📖	mathematical	—	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AdicCompletion DFinsupp.instDFunLike LinearMap Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring DirectSum AddCommGroup.toAddCommMonoid DirectSum.instAddCommGroup DirectSum.instModule instAddCommGroup instAddCommMonoidDirectSum module LinearMap.instFunLike sumInv map DirectSum.component	—	induction_on IsScalarTower.left
sumInv_comp_sum 📖	mathematical	—	LinearMap.comp AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring DirectSum AddCommGroup.toAddCommMonoid instAddCommGroup DirectSum.instAddCommGroup DirectSum.instModule instCommRing instAddCommMonoidDirectSum module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids sumInv sum LinearMap.id	—	DirectSum.linearMap_ext RingHomCompTriple.ids map_ext' DirectSum.ext_component IsScalarTower.left ext sum_lof component_sumInv DirectSum.component.of
sum_comp_sumInv 📖	mathematical	—	LinearMap.comp AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring DirectSum AddCommGroup.toAddCommMonoid DirectSum.instAddCommGroup DirectSum.instModule instAddCommGroup instCommRing instAddCommMonoidDirectSum module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids sum sumInv LinearMap.id	—	map_ext' RingHomCompTriple.ids ext IsScalarTower.left DirectSum.sum_univ_of Finset.sum_congr sumInv_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sum_of val_sum_apply
sum_lof 📖	mathematical	—	DFunLike.coe LinearMap AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring DirectSum AddCommGroup.toAddCommMonoid instAddCommGroup DirectSum.instAddCommGroup DirectSum.instModule instAddCommMonoidDirectSum module LinearMap.instFunLike sum DirectSum.lof map	—	DirectSum.toModule_lof
sum_of 📖	mathematical	—	DFunLike.coe LinearMap AdicCompletion Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.id Semiring.toNonAssocSemiring DirectSum AddCommGroup.toAddCommMonoid instAddCommGroup DirectSum.instAddCommGroup DirectSum.instModule instAddCommMonoidDirectSum module LinearMap.instFunLike sum AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike DirectSum.of map DirectSum.lof	—	IsScalarTower.left DirectSum.lof_eq_of sum_lof
transitionMap_comp_reduceModIdeal 📖	mathematical	—	LinearMap.comp HasQuotient.Quotient Submodule Ring.toSemiring CommRing.toRing AddCommGroup.toAddCommMonoid Submodule.hasQuotient Ideal Submodule.instSMul Semiring.toModule 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 RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids transitionMap LinearMap.restrictScalars CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 IsScalarTower.right Algebra.id Ideal.Quotient.semiring Module.instQuotientIdealSubmoduleHSMulTop Ideal.instIsTwoSided_1 LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Submodule.Quotient.instSMul Ring.toAddCommGroup Module.IsTorsionBySet.isScalarTower Module.isTorsionBySet_quotient_ideal_smul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instDistribSMul Submodule.Quotient.isScalarTower SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap.reduceModIdeal	—	Submodule.linearMap_qext IsScalarTower.left RingHomCompTriple.ids IsScalarTower.right Ideal.instIsTwoSided_1 LinearMap.IsScalarTower.compatibleSMul Module.IsTorsionBySet.isScalarTower Module.isTorsionBySet_quotient_ideal_smul Submodule.Quotient.isScalarTower LinearMap.ext

AdicCompletion.AdicCauchySequence

Definitions

Name	Category	Theorems
map 📖	CompOp	6 math math: map_zero, map_id, AdicCompletion.map_mk, map_apply_coe, map_comp_apply, map_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_apply_coe 📖	mathematical	—	AdicCompletion.IsAdicCauchy DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AdicCompletion.AdicCauchySequence AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike map	—	—
map_comp 📖	mathematical	—	LinearMap.comp AdicCompletion.AdicCauchySequence CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids map	—	RingHomCompTriple.ids
map_comp_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AdicCompletion.AdicCauchySequence AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike map LinearMap.comp RingHomCompTriple.ids	—	—
map_id 📖	mathematical	—	map LinearMap.id CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AdicCompletion.AdicCauchySequence instAddCommGroup instModule	—	—
map_zero 📖	mathematical	—	map LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instZero AdicCompletion.AdicCauchySequence instAddCommGroup instModule	—	—

LinearMap

Definitions

Name	Category	Theorems
reduceModIdeal 📖	CompOp	4 math math: AdicCompletion.map_val_apply, AdicCompletion.pi_apply_coe, AdicCompletion.transitionMap_comp_reduceModIdeal, reduceModIdeal_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reduceModIdeal_apply 📖	mathematical	—	DFunLike.coe LinearMap HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.semiring RingHom.id Semiring.toNonAssocSemiring Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop Ring.toSemiring Submodule.Quotient.addCommGroup Module.instQuotientIdealSubmoduleHSMulTop Ideal.instIsTwoSided_1 instFunLike reduceModIdeal	—	IsScalarTower.left Ideal.instIsTwoSided_1

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
surjective_of_mkQ_comp_surjective 📖	—	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 Top.top Submodule.instTop DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike LinearMap.comp RingHomCompTriple.ids Submodule.mkQ	—	—	IsScalarTower.left RingHomCompTriple.ids AdicCompletion.map_surjective_of_mkQ_comp_surjective AdicCompletion.of_surjective AdicCompletion.map_of
surjective_of_mk_map_comp_surjective 📖	—	HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.map RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike DFunLike.coe Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.comp	—	—	Ideal.instIsTwoSided_1 IsScalarTower.right RingHomCompTriple.ids IsScalarTower.left Ideal.smul_top_eq_map IsHausdorff.map_algebraMap_iff surjective_of_mkQ_comp_surjective

---

← Back to Index