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_lof, 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, lequivCongrLeft_lof, lequivCongrLeft_symm_lof, lequivProdDirectSum_apply, lequivProdDirectSum_symm_apply, lid_apply, lid_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	80
Total	101

DirectSum

Definitions

Name	Category	Theorems
coeFnLinearMap 📖	CompOp	3 math math: ker_lmap, coeFnLinearMap_apply, range_lmap
coeLinearMap 📖	CompOp	11 math math: IsInternal.ofBijective_coeLinearMap_same, MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum, coeLinearMap_lof, 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	163 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, lid_apply, TensorProduct.gradedMul_def, bracket_apply_apply, MultilinearMap.fromDirectSumEquiv_symm_apply, GradedTensorProduct.auxEquiv_one, Module.DirectLimit.quotMk_of, IsBaseChange.directSumPow, TensorProduct.gradedComm_algebraMap_tmul, instSMulCommClass, IsBaseChange.directSum, instLieModule, coeLinearMap_lof, 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, lid_symm_apply, GradedTensorProduct.auxEquiv_symm_one, sigmaLcurry_apply, GradedTensorProduct.auxEquiv_comm, LieDerivation.ofGradingSum_of, 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, decomposeLinearEquiv_apply_coe, 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, lequivCongrLeft_symm_lof, 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, decomposeLinearEquiv_symm_lof, lmap_injective, PiTensorProduct.ofDirectSumEquiv_tprod_apply, toModule.unique, TensorProduct.one_gradedMul, lequivCongrLeft_lof, 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, TensorProduct.coe_directSumRight, 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, TensorProduct.restrictScalar_directSumRight, Module.Free.directSum
lequivCongrLeft 📖	CompOp	3 math math: lequivCongrLeft_apply, lequivCongrLeft_symm_lof, lequivCongrLeft_lof
lequivProdDirectSum 📖	CompOp	2 math math: lequivProdDirectSum_symm_apply, lequivProdDirectSum_apply
lid 📖	CompOp	2 math math: lid_apply, lid_symm_apply
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	49 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, coeLinearMap_lof, AdicCompletion.sum_lof, PiTensorProduct.ofDirectSumEquiv_symm_lof_tprod, lid_symm_apply, 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, decomposeLinearEquiv_apply_coe, 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, lequivCongrLeft_symm_lof, TensorProduct.tmul_of_gradedMul_of_tmul, TensorProduct.gradedCommAux_lof_tmul, linearEquivFunOnFintype_symm_single, decomposeLinearEquiv_symm_lof, toModule.unique, lequivCongrLeft_lof, 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_lof 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid instAddCommMonoidDirectSum instModule Submodule.module LinearMap.instFunLike coeLinearMap lof	—	coeLinearMap_of
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	IsCentralScalar DirectSum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instModule MulOpposite MulOpposite.instMonoid MulOpposite.instSemiring	—	—
instIsScalarTower 📖	mathematical	IsScalarTower SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	IsScalarTower DirectSum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instModule	—	—
instSMulCommClass 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	SMulCommClass DirectSum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instModule	—	—
isInternal_biSup_submodule_of_iSupIndep 📖	mathematical	iSupIndep Set.Elem Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice Set Set.instMembership	IsInternal Set.Elem Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set Set.instMembership 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 Ring.toSemiring AddCommGroup.toAddCommMonoid 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
lequivCongrLeft_lof 📖	mathematical	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm instAddCommMonoidDirectSum instModule DFinsupp.instEquivLikeLinearEquiv lequivCongrLeft LinearMap LinearMap.instFunLike lof	—	RingHomInvPair.ids ext lequivCongrLeft_apply of_apply EquivLike.toEmbeddingLike
lequivCongrLeft_symm_lof 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm instAddCommMonoidDirectSum instModule DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm lequivCongrLeft LinearMap LinearMap.instFunLike lof	—	RingHomInvPair.ids LinearEquiv.symm_apply_eq lequivCongrLeft_lof
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
lid_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum instAddCommMonoidDirectSum instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv lid DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike Unique.instInhabited	—	id_apply
lid_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum instAddCommMonoidDirectSum instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm lid LinearMap LinearMap.instFunLike lof decidableEq_of_subsingleton Unique.instSubsingleton Unique.instInhabited	—	id_symm_apply
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 AddCommGroup.toAddGroup 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 AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid 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 Submodule SetLike.instMembership Submodule.setLike 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	Submodule SetLike.instMembership Submodule.setLike 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 SetLike.instMembership Submodule.setLike 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 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 Submodule SetLike.instMembership Submodule.setLike 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 Submodule SetLike.instMembership Submodule.setLike 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 Submodule SetLike.instMembership Submodule.setLike 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 Submodule SetLike.instMembership Submodule.setLike 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 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 Submodule 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