Module

📁 Source: Mathlib/Algebra/DirectSum/Module.lean

Statistics

Metric	Count
Definitions collectedBasis, coeFnLinearMap, coeLinearMap, component, congrAddEquiv, congrLinearEquiv, congr_addEquiv, congr_linearEquiv, instModule, lequivCongrLeft, lequivProdDirectSum, lid, linearEquivFunOnFintype, lmap, lmk, lof, lsetToSet, sigmaLcurry, sigmaLcurryEquiv, sigmaLuncurry, toModule	21
Theorems addSubgroup_iSupIndep, addSubmonoid_iSupIndep, collectedBasis_coe, collectedBasis_mem, collectedBasis_repr_of_mem, collectedBasis_repr_of_mem_ne, isCompl, ofBijective_coeLinearMap_of_mem, ofBijective_coeLinearMap_of_mem_ne, ofBijective_coeLinearMap_of_ne, ofBijective_coeLinearMap_same, submodule_iSupIndep, submodule_iSup_eq_top, apply_eq_component, coeFnLinearMap_apply, coeLinearMap_eq_dfinsuppSum, coeLinearMap_of, coe_congrAddEquiv, coe_congrLinearEquiv, coe_congr_addEquiv, coe_congr_linearEquiv, coe_toModule_eq_coe_toAddMonoid, lof_self, of, congrLinearEquiv_toAddEquiv, congrLinearEquiv_toLinearMap, congr_linearEquiv_toAddEquiv, congr_linearEquiv_toLinearMap, ext_component, ext_component_iff, instIsCentralScalar, instIsScalarTower, instSMulCommClass, isInternal_biSup_submodule_of_iSupIndep, isInternal_ne_bot_iff, isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, isInternal_submodule_iff_isCompl, isInternal_submodule_of_iSupIndep_of_iSup_eq_top, ker_lmap, ker_map, lequivCongrLeft_apply, lequivProdDirectSum_apply, lequivProdDirectSum_symm_apply, linearEquivFunOnFintype_apply, linearEquivFunOnFintype_lof, linearEquivFunOnFintype_symm_coe, linearEquivFunOnFintype_symm_single, linearMap_ext, linearMap_ext_iff, lmap_apply, lmap_comp, lmap_eq_iff, lmap_eq_map, lmap_id, lmap_injective, lmap_lof, lmap_of, lmap_surjective, lof_apply, lof_eq_of, mk_smul, mker_map, mrange_map, of_smul, range_coeLinearMap, range_lmap, range_map, sigmaLcurry_apply, sigmaLuncurry_apply, single_eq_lof, smul_apply, support_smul, toAddMonoidHom_lmap, unique, toModule_lof	75
Total	96

DirectSum

Definitions

Name	Category	Theorems
coeFnLinearMap 📖	CompOp	3 math math: ker_lmap, coeFnLinearMap_apply, range_lmap
coeLinearMap 📖	CompOp	10 math math: IsInternal.ofBijective_coeLinearMap_same, MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum, coeLinearMap_of, coeLinearMap_eq_dfinsuppSum, IsInternal.ofBijective_coeLinearMap_of_mem_ne, IsInternal.ofBijective_coeLinearMap_of_mem, MvPolynomial.weightedHomogeneousComponent_directSum, MvPolynomial.DirectSum.coeLinearMap_eq_finsum, IsInternal.ofBijective_coeLinearMap_of_ne, range_coeLinearMap
component 📖	CompOp	7 math math: component.of, AdicCompletion.sumInv_apply, lieAlgebraComponent_apply, ext_component_iff, component.lof_self, apply_eq_component, AdicCompletion.component_sumInv
congrAddEquiv 📖	CompOp	4 math math: coe_congr_addEquiv, congr_linearEquiv_toAddEquiv, congrLinearEquiv_toAddEquiv, coe_congrAddEquiv
congrLinearEquiv 📖	CompOp	6 math math: congr_linearEquiv_toAddEquiv, coe_congr_linearEquiv, congr_linearEquiv_toLinearMap, congrLinearEquiv_toLinearMap, congrLinearEquiv_toAddEquiv, coe_congrLinearEquiv
congr_addEquiv 📖	CompOp	—
congr_linearEquiv 📖	CompOp	—
instModule 📖	CompOp	152 math math: IsInternal.ofBijective_coeLinearMap_same, MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum, component.of, coe_toModule_eq_coe_toAddMonoid, lmap_id, PiTensorProduct.ofDirectSumEquiv_tprod_lof, Module.Presentation.directSum_var, ModuleCat.ι_coprodIsoDirectSum_hom_apply, of_smul, instIsCentralScalar, TensorProduct.gradedComm_tmul_one, LinearAlgebra.FreeProduct.mul_injections, Representation.directSum_apply, TensorProduct.gradedMul_assoc, TensorProduct.directSum_lof_tmul_lof, lequivCongrLeft_apply, lmap_apply, lmap_comp, rank_directSum, TensorProduct.coe_directSumRight', mk_smul, Module.equiv_directSum_of_isTorsion, TensorProduct.gradedMul_def, MultilinearMap.fromDirectSumEquiv_symm_apply, GradedTensorProduct.auxEquiv_one, Module.DirectLimit.quotMk_of, IsBaseChange.directSumPow, TensorProduct.gradedComm_algebraMap_tmul, instSMulCommClass, IsBaseChange.directSum, instLieModule, ker_lmap, AdicCompletion.sumInv_apply, Module.Presentation.directSum_relation, coeLinearMap_of, AdicCompletion.sum_lof, coeLinearMap_eq_dfinsuppSum, ExteriorAlgebra.GradedAlgebra.ι_sq_zero, PiTensorProduct.ofDirectSumEquiv_symm_lof_tprod, TensorProduct.directSumRight_comp_rTensor, GradedTensorProduct.auxEquiv_symm_one, sigmaLcurry_apply, GradedTensorProduct.auxEquiv_comm, congr_linearEquiv_toAddEquiv, TensorProduct.gradedComm_algebraMap, ModuleCat.lof_coprodIsoDirectSum_inv, TensorProduct.gradedComm_tmul_of_zero, Module.Relations.Solution.directSum_var, Module.Presentation.directSum_G, lof_eq_of, lmap_eq_map, coe_congr_linearEquiv, TensorProduct.directSumLeft_tmul_lof, lieAlgebraComponent_apply, AdicCompletion.sumInv_comp_sum, TensorProduct.algebraMap_gradedMul, congr_linearEquiv_toLinearMap, IsInternal.ofBijective_coeLinearMap_of_mem_ne, TensorProduct.gradedComm_one, linearEquivFunOnFintype_lof, TensorProduct.gradedComm_symm, CliffordAlgebra.GradedAlgebra.ι_apply, GradedTensorProduct.auxEquiv_mul, congrLinearEquiv_toLinearMap, ModuleCat.lof_coprodIsoDirectSum_inv_apply, lmap_surjective, lmap_lof, LinearAlgebra.FreeProduct.identify_one, linearMap_ext_iff, TensorProduct.gradedMul_one, ext_component_iff, Module.Relations.Solution.IsPresentation.directSum, Module.Finite.instDirectSum, GradedTensorProduct.mulHom_apply, MultilinearMap.fromDirectSumEquiv_lof, TensorProduct.directSumRight_tmul_lof, IsInternal.ofBijective_coeLinearMap_of_mem, MvPolynomial.weightedHomogeneousComponent_directSum, TensorProduct.directSumLeft_symm_lof_tmul, component.lof_self, AdicCompletion.sum_of, single_eq_lof, MultilinearMap.fromDirectSumEquiv_apply, finsuppLEquivDirectSum_single, GradedTensorProduct.auxEquiv_tmul, decomposeLinearEquiv_apply, TensorProduct.gradedComm_of_zero_tmul, ModuleCat.ι_coprodIsoDirectSum_hom, decomposeLinearEquiv_symm_comp_lof, TensorProduct.directSumLeft_tmul, MvPolynomial.DirectSum.coeLinearMap_eq_finsum, TensorAlgebra.GradedAlgebra.ι_apply, decomposeLinearEquiv_symm_apply, LinearAlgebra.FreeProduct.rel_id, Module.equiv_free_prod_directSum, TensorProduct.directSum_symm_lof_tmul, toModule_lof, MultilinearMap.directSum_ext_iff, TensorProduct.directSumRight_tmul, TensorProduct.gradedComm_tmul_algebraMap, sigmaLuncurry_apply, finsuppLEquivDirectSum_apply, lof_apply, apply_eq_component, TensorProduct.directSumRight'_restrict, Module.finrank_directSum, coeFnLinearMap_apply, TensorProduct.gradedMul_algebraMap, AdicCompletion.sumEquivOfFintype_apply, Module.Flat.directSum, TensorProduct.gradedCommAux_comp_gradedCommAux, HahnEmbedding.Seed.hahnCoeff_apply, range_lmap, TensorProduct.tmul_of_gradedMul_of_tmul, TensorProduct.gradedComm_one_tmul, support_smul, congrLinearEquiv_toAddEquiv, smul_apply, IsInternal.ofBijective_coeLinearMap_of_ne, TensorProduct.gradedCommAux_lof_tmul, AdicCompletion.component_sumInv, linearEquivFunOnFintype_symm_single, Module.Presentation.directSum_R, lmap_of, lmap_injective, PiTensorProduct.ofDirectSumEquiv_tprod_apply, toModule.unique, TensorProduct.one_gradedMul, Module.FaithfullyFlat.directSum, lmap_finsuppLEquivDirectSum_eq, ExteriorAlgebra.GradedAlgebra.ι_apply, CliffordAlgebra.GradedAlgebra.ι_sq_scalar, TensorProduct.gradedComm_of_tmul_of, AdicCompletion.sumEquivOfFintype_symm_apply, Module.torsion_by_prime_power_decomposition, toLieAlgebra_apply, TensorProduct.gradedComm_gradedMul, toAddMonoidHom_lmap, Module.Flat.directSum_iff, instIsScalarTower, TensorProduct.directSumRight_symm_lof_tmul, decompose_smul, lmap_eq_iff, range_coeLinearMap, lequivProdDirectSum_symm_apply, linearEquivFunOnFintype_symm_coe, linearEquivFunOnFintype_apply, finsuppLEquivDirectSum_symm_lof, AdicCompletion.sum_comp_sumInv, coe_congrLinearEquiv, lequivProdDirectSum_apply, Module.Free.directSum
lequivCongrLeft 📖	CompOp	1 math math: lequivCongrLeft_apply
lequivProdDirectSum 📖	CompOp	2 math math: lequivProdDirectSum_symm_apply, lequivProdDirectSum_apply
lid 📖	CompOp	—
linearEquivFunOnFintype 📖	CompOp	4 math math: linearEquivFunOnFintype_lof, linearEquivFunOnFintype_symm_single, linearEquivFunOnFintype_symm_coe, linearEquivFunOnFintype_apply
lmap 📖	CompOp	21 math math: lmap_id, Representation.directSum_apply, lmap_apply, lmap_comp, IsBaseChange.directSumPow, IsBaseChange.directSum, ker_lmap, TensorProduct.directSumRight_comp_rTensor, lmap_eq_map, coe_congr_linearEquiv, congr_linearEquiv_toLinearMap, congrLinearEquiv_toLinearMap, lmap_surjective, lmap_lof, range_lmap, lmap_of, lmap_injective, lmap_finsuppLEquivDirectSum_eq, toAddMonoidHom_lmap, lmap_eq_iff, coe_congrLinearEquiv
lmk 📖	CompOp	—
lof 📖	CompOp	43 math math: component.of, PiTensorProduct.ofDirectSumEquiv_tprod_lof, Module.Presentation.directSum_var, ModuleCat.ι_coprodIsoDirectSum_hom_apply, LinearAlgebra.FreeProduct.mul_injections, TensorProduct.directSum_lof_tmul_lof, MultilinearMap.fromDirectSumEquiv_symm_apply, AdicCompletion.sum_lof, PiTensorProduct.ofDirectSumEquiv_symm_lof_tprod, ModuleCat.lof_coprodIsoDirectSum_inv, TensorProduct.gradedComm_tmul_of_zero, Module.Relations.Solution.directSum_var, lof_eq_of, TensorProduct.directSumLeft_tmul_lof, linearEquivFunOnFintype_lof, ModuleCat.lof_coprodIsoDirectSum_inv_apply, lmap_lof, LinearAlgebra.FreeProduct.identify_one, linearMap_ext_iff, LinearAlgebra.FreeProduct.ι_def, MultilinearMap.fromDirectSumEquiv_lof, TensorProduct.directSumRight_tmul_lof, algHom_ext'_iff, TensorProduct.directSumLeft_symm_lof_tmul, component.lof_self, AdicCompletion.sum_of, single_eq_lof, finsuppLEquivDirectSum_single, TensorProduct.gradedComm_of_zero_tmul, ModuleCat.ι_coprodIsoDirectSum_hom, decomposeLinearEquiv_symm_comp_lof, LinearAlgebra.FreeProduct.rel_id, TensorProduct.directSum_symm_lof_tmul, toModule_lof, MultilinearMap.directSum_ext_iff, lof_apply, TensorProduct.tmul_of_gradedMul_of_tmul, TensorProduct.gradedCommAux_lof_tmul, linearEquivFunOnFintype_symm_single, toModule.unique, TensorProduct.gradedComm_of_tmul_of, TensorProduct.directSumRight_symm_lof_tmul, finsuppLEquivDirectSum_symm_lof
lsetToSet 📖	CompOp	—
sigmaLcurry 📖	CompOp	1 math math: sigmaLcurry_apply
sigmaLcurryEquiv 📖	CompOp	—
sigmaLuncurry 📖	CompOp	1 math math: sigmaLuncurry_apply
toModule 📖	CompOp	5 math math: coe_toModule_eq_coe_toAddMonoid, toModule_lof, LinearAlgebra.FreeProduct.lift_apply, toModule.unique, toLieAlgebra_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_component 📖	mathematical	—	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike component	—	—
coeFnLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum Pi.addCommMonoid instModule Pi.module LinearMap.instFunLike coeFnLinearMap DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike	—	—
coeLinearMap_eq_dfinsuppSum 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid instAddCommMonoidDirectSum instModule Submodule.module LinearMap.instFunLike coeLinearMap DFinsupp.sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	DFinsupp.sumAddHom_apply
coeLinearMap_of 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid instAddCommMonoidDirectSum instModule Submodule.module LinearMap.instFunLike coeLinearMap AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike of	—	toAddMonoid_of DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
coe_congrAddEquiv 📖	mathematical	—	DFunLike.coe AddMonoidHom DirectSum AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom.instFunLike AddEquiv.toAddMonoidHom congrAddEquiv map	—	—
coe_congrLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum instAddCommMonoidDirectSum instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv congrLinearEquiv LinearMap LinearMap.instFunLike lmap LinearEquiv.toLinearMap	—	RingHomInvPair.ids
coe_congr_addEquiv 📖	mathematical	—	DFunLike.coe AddMonoidHom DirectSum AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom.instFunLike AddEquiv.toAddMonoidHom congrAddEquiv map	—	coe_congrAddEquiv
coe_congr_linearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum instAddCommMonoidDirectSum instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv congrLinearEquiv LinearMap LinearMap.instFunLike lmap LinearEquiv.toLinearMap	—	coe_congrLinearEquiv
coe_toModule_eq_coe_toAddMonoid 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike toModule AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike toAddMonoid LinearMap.toAddMonoidHom	—	—
congrLinearEquiv_toAddEquiv 📖	mathematical	—	LinearEquiv.toAddEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum instAddCommMonoidDirectSum instModule congrLinearEquiv congrAddEquiv	—	RingHomInvPair.ids
congrLinearEquiv_toLinearMap 📖	mathematical	—	LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum instAddCommMonoidDirectSum instModule congrLinearEquiv lmap	—	RingHomInvPair.ids
congr_linearEquiv_toAddEquiv 📖	mathematical	—	LinearEquiv.toAddEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum instAddCommMonoidDirectSum instModule congrLinearEquiv congrAddEquiv	—	congrLinearEquiv_toAddEquiv
congr_linearEquiv_toLinearMap 📖	mathematical	—	LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum instAddCommMonoidDirectSum instModule congrLinearEquiv lmap	—	congrLinearEquiv_toLinearMap
ext_component 📖	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike component	—	—	DFinsupp.ext
ext_component_iff 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike component	—	ext_component
instIsCentralScalar 📖	mathematical	IsCentralScalar SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulOpposite MulOpposite.instMonoid MulOpposite.instSemiring	DirectSum instAddCommMonoidDirectSum instModule	—	DFinsupp.isCentralScalar
instIsScalarTower 📖	mathematical	IsScalarTower SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	DirectSum instAddCommMonoidDirectSum instModule	—	DFinsupp.isScalarTower
instSMulCommClass 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	DirectSum instAddCommMonoidDirectSum instModule	—	DFinsupp.smulCommClass
isInternal_biSup_submodule_of_iSupIndep 📖	mathematical	iSupIndep Set.Elem Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice Set Set.instMembership	IsInternal SetLike.instMembership Submodule.setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.addCommMonoid Submodule.module Submodule.addSubmonoidClass Submodule.comap RingHom.id Semiring.toNonAssocSemiring Submodule.subtype	—	Submodule.addSubmonoidClass isInternal_submodule_iff_iSupIndep_and_iSup_eq_top le_biSup Submodule.ext RingHomSurjective.ids Submodule.map_comap_subtype inf_of_le_right iSupIndep_map_orderIso_iff iSupIndep.of_coe_Iic_comp iSup_subtype iSup_congr_Prop Submodule.biSup_comap_subtype_eq_top
isInternal_ne_bot_iff 📖	mathematical	—	IsInternal Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Bot.bot Submodule.instBot Submodule.setLike Submodule.addSubmonoidClass	—	Submodule.addSubmonoidClass iSup_ne_bot_subtype
isInternal_submodule_iff_iSupIndep_and_iSup_eq_top 📖	mathematical	—	IsInternal Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike Submodule.addSubmonoidClass iSupIndep Submodule.completeLattice iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Top.top Submodule.instTop	—	Submodule.addSubmonoidClass IsInternal.submodule_iSupIndep IsInternal.submodule_iSup_eq_top isInternal_submodule_of_iSupIndep_of_iSup_eq_top
isInternal_submodule_iff_isCompl 📖	mathematical	Set.univ Set Set.instInsert Set.instSingletonSet	IsInternal Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike Submodule.addSubmonoidClass IsCompl Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice	—	Set.ext_iff Submodule.addSubmonoidClass isInternal_submodule_iff_iSupIndep_and_iSup_eq_top iSup.eq_1 Set.image_univ Set.image_insert_eq Set.image_singleton sSup_pair iSupIndep_pair codisjoint_iff Codisjoint.eq_top
isInternal_submodule_of_iSupIndep_of_iSup_eq_top 📖	mathematical	iSupIndep Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Top.top Submodule.instTop	IsInternal Submodule.setLike Submodule.addSubmonoidClass	—	Submodule.addSubmonoidClass iSupIndep.dfinsupp_lsum_injective RingHomSurjective.ids RingHomInvPair.ids AddMonoid.nat_smulCommClass' LinearMap.range_eq_top Submodule.iSup_eq_range_dfinsupp_lsum
ker_lmap 📖	mathematical	—	LinearMap.ker DirectSum instAddCommMonoidDirectSum instModule RingHom.id Semiring.toNonAssocSemiring lmap Submodule.comap Pi.addCommMonoid Pi.module coeFnLinearMap Submodule.pi Set.univ	—	DFinsupp.ker_mapRangeLinearMap
ker_map 📖	mathematical	—	AddMonoidHom.ker DirectSum AddCommGroup.toAddCommMonoid AddCommGroup.toAddGroup instAddCommGroup AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum map AddSubgroup.comap Pi.addGroup coeFnAddMonoidHom AddSubgroup.pi Set.univ	—	DFinsupp.ker_mapRangeAddMonoidHom
lequivCongrLeft_apply 📖	mathematical	—	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm DFinsupp.instDFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum instAddCommMonoidDirectSum instModule DFinsupp.instEquivLikeLinearEquiv lequivCongrLeft	—	equivCongrLeft_apply
lequivProdDirectSum_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum instAddCommMonoidDirectSum Prod.instAddCommMonoid instModule Prod.instModule EquivLike.toFunLike LinearEquiv.instEquivLike lequivProdDirectSum Equiv.toFun AddEquiv.toEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Prod.instAdd addEquivProdDirectSum	—	RingHomInvPair.ids
lequivProdDirectSum_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum Prod.instAddCommMonoid instAddCommMonoidDirectSum Prod.instModule instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm lequivProdDirectSum Equiv.invFun AddEquiv.toEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Prod.instAdd addEquivProdDirectSum	—	RingHomInvPair.ids
linearEquivFunOnFintype_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum instAddCommMonoidDirectSum Pi.addCommMonoid instModule Pi.module EquivLike.toFunLike LinearEquiv.instEquivLike linearEquivFunOnFintype DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike	—	RingHomInvPair.ids
linearEquivFunOnFintype_lof 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum instAddCommMonoidDirectSum Pi.addCommMonoid instModule Pi.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv linearEquivFunOnFintype LinearMap LinearMap.instFunLike lof Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids
linearEquivFunOnFintype_symm_coe 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum Pi.addCommMonoid instAddCommMonoidDirectSum Pi.module instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm linearEquivFunOnFintype DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike	—	LinearEquiv.symm_apply_apply RingHomInvPair.ids
linearEquivFunOnFintype_symm_single 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum Pi.addCommMonoid instAddCommMonoidDirectSum Pi.module instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm linearEquivFunOnFintype Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearMap LinearMap.instFunLike lof	—	DFinsupp.equivFunOnFintype_symm_single
linearMap_ext 📖	—	LinearMap.comp DirectSum instAddCommMonoidDirectSum instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids lof	—	—	RingHomCompTriple.ids DFinsupp.lhom_ext'
linearMap_ext_iff 📖	mathematical	—	LinearMap.comp DirectSum instAddCommMonoidDirectSum instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids lof	—	RingHomCompTriple.ids linearMap_ext
lmap_apply 📖	mathematical	—	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike lmap	—	—
lmap_comp 📖	mathematical	—	lmap LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DirectSum instAddCommMonoidDirectSum instModule	—	DFinsupp.mapRange.linearMap_comp
lmap_eq_iff 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike lmap DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike	—	map_eq_iff
lmap_eq_map 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike lmap AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike map LinearMap.toAddMonoidHom	—	—
lmap_id 📖	mathematical	—	lmap LinearMap.id DirectSum instAddCommMonoidDirectSum instModule	—	DFinsupp.mapRange.linearMap_id
lmap_injective 📖	mathematical	—	DirectSum DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoidDirectSum instModule LinearMap.instFunLike lmap	—	DFinsupp.mapRange_injective map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
lmap_lof 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike lmap lof	—	DFinsupp.mapRange_single map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
lmap_of 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike lmap AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike of	—	DFinsupp.mapRange_single map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
lmap_surjective 📖	mathematical	—	DirectSum DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoidDirectSum instModule LinearMap.instFunLike lmap	—	DFinsupp.mapRange_surjective map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
lof_apply 📖	mathematical	—	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike lof	—	DFinsupp.single_eq_same
lof_eq_of 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike lof AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike of	—	—
mk_smul 📖	mathematical	—	DFunLike.coe AddMonoidHom DirectSum AddZeroClass.toAddZero Pi.addZeroClass Set.Elem SetLike.coe Finset Finset.instSetLike Set Set.instMembership AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom.instFunLike Pi.instSMul SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instModule	—	LinearMap.map_smul
mker_map 📖	mathematical	—	AddMonoidHom.mker DirectSum AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom AddZeroClass.toAddZero AddMonoidHom.instFunLike AddMonoidHom.instAddMonoidHomClass map AddSubmonoid.comap Pi.addZeroClass coeFnAddMonoidHom AddSubmonoid.pi Set.univ	—	DFinsupp.mker_mapRangeAddMonoidHom
mrange_map 📖	mathematical	—	AddMonoidHom.mrange DirectSum AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom AddZeroClass.toAddZero AddMonoidHom.instFunLike AddMonoidHom.instAddMonoidHomClass map AddSubmonoid.comap Pi.addZeroClass coeFnAddMonoidHom AddSubmonoid.pi Set.univ	—	DFinsupp.mrange_mapRangeAddMonoidHom
of_smul 📖	mathematical	—	DFunLike.coe AddMonoidHom DirectSum AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom.instFunLike of SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instModule	—	LinearMap.map_smul
range_coeLinearMap 📖	mathematical	—	LinearMap.range DirectSum Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid instAddCommMonoidDirectSum instModule Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids coeLinearMap iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	—	RingHomSurjective.ids RingHomInvPair.ids AddMonoid.nat_smulCommClass' Submodule.iSup_eq_range_dfinsupp_lsum
range_lmap 📖	mathematical	—	LinearMap.range DirectSum instAddCommMonoidDirectSum instModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids lmap Submodule.comap Pi.addCommMonoid Pi.module coeFnLinearMap Submodule.pi Set.univ	—	DFinsupp.range_mapRangeLinearMap
range_map 📖	mathematical	—	AddMonoidHom.range DirectSum AddCommGroup.toAddCommMonoid AddCommGroup.toAddGroup instAddCommGroup map AddSubgroup.comap Pi.addGroup coeFnAddMonoidHom AddSubgroup.pi Set.univ	—	DFinsupp.range_mapRangeAddMonoidHom
sigmaLcurry_apply 📖	mathematical	—	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike DirectSum LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoidDirectSum instModule LinearMap.instFunLike sigmaLcurry	—	sigmaCurry_apply
sigmaLuncurry_apply 📖	mathematical	—	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike sigmaLuncurry	—	sigmaUncurry_apply
single_eq_lof 📖	mathematical	—	DFinsupp.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike lof	—	—
smul_apply 📖	mathematical	—	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike DirectSum SMulZeroClass.toSMul instAddCommMonoidDirectSum DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instModule	—	DFinsupp.smul_apply
support_smul 📖	mathematical	—	Finset Finset.instHasSubset DFinsupp.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DirectSum SMulZeroClass.toSMul instAddCommMonoidDirectSum DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instModule	—	DFinsupp.support_smul
toAddMonoidHom_lmap 📖	mathematical	—	LinearMap.toAddMonoidHom DirectSum instAddCommMonoidDirectSum instModule RingHom.id Semiring.toNonAssocSemiring lmap map	—	—
toModule_lof 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum instModule LinearMap.instFunLike toModule lof	—	toAddMonoid_of

DirectSum.IsInternal

Definitions

Name	Category	Theorems
collectedBasis 📖	CompOp	7 math math: collectedBasis_mem, collectedBasis_coe, collectedBasis_orthonormal, collectedBasis_repr_of_mem_ne, LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal', LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne, collectedBasis_repr_of_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addSubgroup_iSupIndep 📖	mathematical	DirectSum.IsInternal AddSubgroup AddCommGroup.toAddGroup AddCommGroup.toAddCommMonoid AddSubgroup.instSetLike AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddSubgroup.instAddSubgroupClass	iSupIndep AddSubgroup.instCompleteLattice	—	AddSubgroupClass.toAddSubmonoidClass AddSubgroup.instAddSubgroupClass iSupIndep_of_dfinsuppSumAddHom_injective' Function.Bijective.injective
addSubmonoid_iSupIndep 📖	mathematical	DirectSum.IsInternal AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.instAddSubmonoidClass	iSupIndep AddSubmonoid.instCompleteLattice	—	AddSubmonoid.instAddSubmonoidClass iSupIndep_of_dfinsuppSumAddHom_injective Function.Bijective.injective
collectedBasis_coe 📖	mathematical	DirectSum.IsInternal Submodule Submodule.setLike Submodule.addSubmonoidClass	DFunLike.coe Module.Basis Module.Basis.instFunLike collectedBasis SetLike.instMembership Submodule.addCommMonoid Submodule.module	—	Submodule.addSubmonoidClass RingHomInvPair.ids sigmaFinsuppEquivDFinsupp_single Module.Basis.repr_symm_apply DFinsupp.mapRange.congr_simp DFinsupp.mapRange_single Finsupp.linearCombination_single one_smul DFinsupp.sumAddHom_single
collectedBasis_mem 📖	mathematical	DirectSum.IsInternal Submodule Submodule.setLike Submodule.addSubmonoidClass	SetLike.instMembership DFunLike.coe Module.Basis Module.Basis.instFunLike collectedBasis	—	Submodule.addSubmonoidClass collectedBasis_coe
collectedBasis_repr_of_mem 📖	mathematical	DirectSum.IsInternal Submodule Submodule.setLike Submodule.addSubmonoidClass SetLike.instMembership	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr collectedBasis Submodule.addCommMonoid Submodule.module	—	Submodule.addSubmonoidClass RingHomInvPair.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass ofBijective_coeLinearMap_of_mem
collectedBasis_repr_of_mem_ne 📖	mathematical	DirectSum.IsInternal Submodule Submodule.setLike Submodule.addSubmonoidClass SetLike.instMembership	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr collectedBasis	—	Submodule.addSubmonoidClass RingHomInvPair.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass ofBijective_coeLinearMap_of_mem_ne
isCompl 📖	mathematical	Set.univ Set Set.instInsert Set.instSingletonSet DirectSum.IsInternal Submodule Submodule.setLike Submodule.addSubmonoidClass	IsCompl Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice	—	Submodule.addSubmonoidClass iSupIndep.pairwiseDisjoint submodule_iSupIndep codisjoint_iff submodule_iSup_eq_top sSup_pair iSup.eq_1 Set.image_univ Set.image_insert_eq Set.image_singleton
ofBijective_coeLinearMap_of_mem 📖	mathematical	DirectSum.IsInternal Submodule Submodule.setLike Submodule.addSubmonoidClass SetLike.instMembership	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum Submodule.addCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm LinearEquiv.ofBijective DirectSum.coeLinearMap	—	Submodule.addSubmonoidClass ofBijective_coeLinearMap_same
ofBijective_coeLinearMap_of_mem_ne 📖	mathematical	DirectSum.IsInternal Submodule Submodule.setLike Submodule.addSubmonoidClass SetLike.instMembership	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum Submodule.addCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm LinearEquiv.ofBijective DirectSum.coeLinearMap Submodule.zero	—	Submodule.addSubmonoidClass ofBijective_coeLinearMap_of_ne
ofBijective_coeLinearMap_of_ne 📖	mathematical	DirectSum.IsInternal Submodule Submodule.setLike Submodule.addSubmonoidClass	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership DFinsupp.instDFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum Submodule.addCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm LinearEquiv.ofBijective DirectSum.coeLinearMap Submodule.zero	—	Submodule.addSubmonoidClass RingHomInvPair.ids DirectSum.coeLinearMap_of LinearEquiv.ofBijective_symm_apply_apply DirectSum.of_eq_of_ne
ofBijective_coeLinearMap_same 📖	mathematical	DirectSum.IsInternal Submodule Submodule.setLike Submodule.addSubmonoidClass	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership DFinsupp.instDFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum Submodule.addCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm LinearEquiv.ofBijective DirectSum.coeLinearMap	—	Submodule.addSubmonoidClass RingHomInvPair.ids DirectSum.coeLinearMap_of LinearEquiv.ofBijective_symm_apply_apply DirectSum.of_eq_same
submodule_iSupIndep 📖	mathematical	DirectSum.IsInternal Submodule Submodule.setLike Submodule.addSubmonoidClass	iSupIndep Submodule.completeLattice	—	Submodule.addSubmonoidClass iSupIndep_of_dfinsupp_lsum_injective Function.Bijective.injective
submodule_iSup_eq_top 📖	mathematical	DirectSum.IsInternal Submodule Submodule.setLike Submodule.addSubmonoidClass	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Top.top Submodule.instTop	—	Submodule.addSubmonoidClass RingHomSurjective.ids RingHomInvPair.ids AddMonoid.nat_smulCommClass' Submodule.iSup_eq_range_dfinsupp_lsum LinearMap.range_eq_top Function.Bijective.surjective

DirectSum.component

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lof_self 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum DirectSum.instModule LinearMap.instFunLike DirectSum.component DirectSum.lof	—	DirectSum.lof_apply
of 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum DirectSum.instModule LinearMap.instFunLike DirectSum.component DirectSum.lof AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	DFinsupp.single_apply

DirectSum.toModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
unique 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum DirectSum.instModule LinearMap.instFunLike DirectSum.toModule LinearMap.comp RingHomCompTriple.ids DirectSum.lof	—	DirectSum.toAddMonoid.unique

---

← Back to Index