PID

📁 Source: Mathlib/LinearAlgebra/FreeModule/PID.lean

Statistics

Metric	Count
Definitions ringBasis, selfBasis, smithCoeffs, smithNormalForm, SmithNormalForm, a, bM, bN, f, basisOfFiniteTypeTorsionFree, basisOfFiniteTypeTorsionFree', basisOfPid, basisOfPidOfLE, basisOfPidOfLESpan, smithNormalForm, smithNormalFormBotBasis, smithNormalFormCoeffs, smithNormalFormOfLE, smithNormalFormOfRankEq, smithNormalFormTopBasis	20
Theorems exists_smith_normal_form, finrank_eq_finrank, selfBasis_def, smithCoeffs_ne_zero, coord_apply_embedding_eq_smul_coord, le_ker_coord_of_notMem_range, repr_apply_embedding_eq_repr_smul, repr_comp_embedding_eq_smul, repr_eq_zero_of_notMem_range, snf, toMatrix_restrict_eq_toMatrix, free_iff_isTorsionFree, free_of_finite_type_torsion_free, free_of_finite_type_torsion_free', basisOfPid_bot, basis_of_pid_aux, exists_smith_normal_form_of_le, exists_smith_normal_form_of_rank_eq, nonempty_basis_of_pid, smithNormalFormBotBasis_def, smithNormalFormCoeffs_ne_zero, dvd_generator_iff, eq_bot_of_generator_maximal_map_eq_zero, eq_bot_of_generator_maximal_submoduleImage_eq_zero, generator_maximal_submoduleImage_dvd, instFreeSubtypeMemIdealOfFiniteOfIsTorsionFree	26
Total	46

Ideal

Definitions

Name	Category	Theorems
ringBasis 📖	CompOp	1 math math: selfBasis_def
selfBasis 📖	CompOp	1 math math: selfBasis_def
smithCoeffs 📖	CompOp	3 math math: selfBasis_def, associated_norm_prod_smith, instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs
smithNormalForm 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_smith_normal_form 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe Module.Basis Submodule.addCommMonoid Submodule.module' Algebra.toSMul Algebra.toModule IsScalarTower.right Module.Basis.instFunLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Submodule.exists_smith_normal_form_of_rank_eq IsScalarTower.right finrank_eq_finrank
finrank_eq_finrank 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetLike.instMembership Submodule.setLike Submodule.restrictScalars Semiring.toModule Algebra.toSMul IsScalarTower.right Submodule.addCommMonoid Submodule.module NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsScalarTower.right nonempty_fintype Module.finrank_eq_card_basis IsNoetherianRing.strongRankCondition IsDomain.toNontrivial PrincipalIdealRing.isNoetherianRing rank_eq LinearMap.IsScalarTower.compatibleSMul Submodule.restrictScalars.isScalarTower Submodule.isScalarTower'
selfBasis_def 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe Module.Basis Submodule.addCommMonoid Submodule.module' Algebra.toSMul Algebra.toModule IsScalarTower.right Module.Basis.instFunLike selfBasis smithCoeffs NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ringBasis	—	IsScalarTower.right exists_smith_normal_form
smithCoeffs_ne_zero 📖	—	—	—	—	Module.Basis.ne_zero IsScalarTower.right IsDomain.toNontrivial Subtype.coe_injective selfBasis_def zero_smul

Module

Definitions

Name	Category	Theorems
basisOfFiniteTypeTorsionFree 📖	CompOp	—
basisOfFiniteTypeTorsionFree' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
free_iff_isTorsionFree 📖	mathematical	—	Free CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid IsTorsionFree	—	Free.instIsTorsionFree free_of_finite_type_torsion_free'
free_of_finite_type_torsion_free 📖	mathematical	Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set.range Top.top Submodule Submodule.instTop	Free	—	nonempty_fintype Free.of_basis
free_of_finite_type_torsion_free' 📖	mathematical	—	Free CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	Free.of_basis

Module.Basis

Definitions

Name	Category	Theorems
SmithNormalForm 📖	CompData	—

Module.Basis.SmithNormalForm

Definitions

Name	Category	Theorems
a 📖	CompOp	6 math math: repr_apply_embedding_eq_repr_smul, snf, toAddSubgroup_index_eq_pow_mul_prod, repr_comp_embedding_eq_smul, toAddSubgroup_index_eq_ite, coord_apply_embedding_eq_smul_coord
bM 📖	CompOp	7 math math: repr_apply_embedding_eq_repr_smul, snf, le_ker_coord_of_notMem_range, repr_comp_embedding_eq_smul, toMatrix_restrict_eq_toMatrix, repr_eq_zero_of_notMem_range, coord_apply_embedding_eq_smul_coord
bN 📖	CompOp	5 math math: repr_apply_embedding_eq_repr_smul, snf, repr_comp_embedding_eq_smul, toMatrix_restrict_eq_toMatrix, coord_apply_embedding_eq_smul_coord
f 📖	CompOp	5 math math: repr_apply_embedding_eq_repr_smul, snf, repr_comp_embedding_eq_smul, toMatrix_restrict_eq_toMatrix, coord_apply_embedding_eq_smul_coord

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coord_apply_embedding_eq_smul_coord 📖	mathematical	—	LinearMap.comp Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule.module Semiring.toModule RingHom.id RingHomCompTriple.ids Module.Basis.coord bM DFunLike.coe Function.Embedding Function.instFunLikeEmbedding f Submodule.subtype LinearMap LinearMap.instSMul instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.to_smulCommClass Algebra.id a bN	—	LinearMap.ext RingHomCompTriple.ids Algebra.to_smulCommClass RingHomInvPair.ids IsScalarTower.left repr_apply_embedding_eq_repr_smul map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Pi.smul_apply
le_ker_coord_of_notMem_range 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding f	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.ker NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id Module.Basis.coord bM	—	repr_eq_zero_of_notMem_range
repr_apply_embedding_eq_repr_smul 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids AddCommGroup.toAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr bM Submodule SetLike.instMembership Submodule.setLike Function.Embedding Function.instFunLikeEmbedding f Submodule.addCommMonoid Submodule.module bN Submodule.smul Algebra.toSMul Algebra.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid a	—	RingHomInvPair.ids IsScalarTower.left Module.Basis.mem_submodule_iff Subtype.coe_eta map_finsuppSum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Module.Basis.repr_self Finsupp.smul_single mul_one Finsupp.sum_single snf Finsupp.sum_apply Finsupp.single_apply Function.instEmbeddingLikeEmbedding Finsupp.sum_ite_eq' mul_comm mul_eq_zero_of_right
repr_comp_embedding_eq_smul 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids AddCommGroup.toAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr bM Submodule SetLike.instMembership Submodule.setLike Function.Embedding Function.instFunLikeEmbedding f Pi.smul' Algebra.toSMul Algebra.id a Submodule.addCommMonoid Submodule.module bN	—	RingHomInvPair.ids IsScalarTower.left repr_apply_embedding_eq_repr_smul map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Pi.smul_apply
repr_eq_zero_of_notMem_range 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding f	Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids AddCommGroup.toAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr bM Submodule SetLike.instMembership Submodule.setLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHomInvPair.ids Module.Basis.mem_submodule_iff snf map_finsuppSum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass Module.Basis.repr_self Finsupp.smul_single mul_one Finsupp.sum_apply Finsupp.single_eq_of_ne' Finsupp.sum_fun_zero
snf 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike DFunLike.coe Module.Basis Submodule.addCommMonoid Submodule.module Module.Basis.instFunLike bN SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction a bM Function.Embedding Function.instFunLikeEmbedding f	—	—
toMatrix_restrict_eq_toMatrix 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	LinearEquiv RingHomInvPair.ids Submodule.addCommMonoid Submodule.module Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Fin.fintype Finite.of_fintype bN LinearMap.restrict bM Function.Embedding Function.instFunLikeEmbedding f	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.toMatrix_apply IsScalarTower.left repr_apply_embedding_eq_repr_smul snf map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass

Submodule

Definitions

Name	Category	Theorems
basisOfPid 📖	CompOp	1 math math: basisOfPid_bot
basisOfPidOfLE 📖	CompOp	—
basisOfPidOfLESpan 📖	CompOp	—
smithNormalForm 📖	CompOp	—
smithNormalFormBotBasis 📖	CompOp	1 math math: smithNormalFormBotBasis_def
smithNormalFormCoeffs 📖	CompOp	1 math math: smithNormalFormBotBasis_def
smithNormalFormOfLE 📖	CompOp	—
smithNormalFormOfRankEq 📖	CompOp	—
smithNormalFormTopBasis 📖	CompOp	1 math math: smithNormalFormBotBasis_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basisOfPid_bot 📖	mathematical	—	basisOfPid Bot.bot Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instBot Module.Basis SetLike.instMembership setLike addCommMonoid module Module.Basis.empty Unique.instSubsingleton uniqueBot Fin.isEmpty'	—	Unique.instSubsingleton Fin.isEmpty' invariantBasisNumber_of_nontrivial_of_commRing IsDomain.toNontrivial Sigma.eq Module.Basis.eq_of_apply_eq Fintype.card_fin Fintype.card_eq_zero Fintype.card_eq
basis_of_pid_aux 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe Module.Basis addCommMonoid module Module.Basis.instFunLike	—	set_has_maximal_iff_noetherian isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing Module.Finite.self Set.mem_range IsPrincipalIdealRing.principal IsPrincipal.generator_mem eq_bot_of_generator_maximal_submoduleImage_eq_zero LinearMap.mem_submoduleImage_of_le generator_maximal_submoduleImage_dvd nonempty_fintype sum_mem smul_mem IsScalarTower.left map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass RingHomInvPair.ids Module.Basis.sum_repr Finset.smul_sum SemigroupAction.mul_smul mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero LinearMap.map_smul mul_one one_ne_zero NeZero.one IsDomain.toNontrivial RingHomSurjective.ids RingHomCompTriple.ids map_subtype_le mem_map Subtype.coe_injective map_add SemilinearMapClass.toAddHomClass LinearMap.mem_ker add_zero map_zero AddMonoidHomClass.toZeroHomClass IsDomain.to_noZeroDivisors mul_eq_zero mul_comm IsPrincipal.generator_submoduleImage_dvd_of_mem sub_mem addSubgroupClass map_sub smul_eq_mul sub_self sub_eq_add_neg neg_smul Module.Basis.coe_mkFinConsOfLE Fin.cons_zero Fin.cons_succ
exists_smith_normal_form_of_le 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership setLike DFunLike.coe Module.Basis addCommMonoid module Module.Basis.instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	nonempty_fintype IsNoetherianRing.strongRankCondition IsDomain.toNontrivial PrincipalIdealRing.isNoetherianRing Unique.instSubsingleton Fin.isEmpty' basis_of_pid_aux Finite.of_fintype
exists_smith_normal_form_of_rank_eq 📖	mathematical	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike addCommMonoid module	DFunLike.coe Module.Basis Module.Basis.instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	nonempty_fintype Fintype.bijective_iff_injective_and_card Function.Embedding.injective Fintype.card_fin Equiv.apply_symm_apply Module.Basis.coe_reindex
nonempty_basis_of_pid 📖	mathematical	—	Module.Basis Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike addCommMonoid module	—	nonempty_fintype IsNoetherianRing.strongRankCondition IsDomain.toNontrivial PrincipalIdealRing.isNoetherianRing RingHomInvPair.ids Unique.instSubsingleton Fin.isEmpty' basis_of_pid_aux Finite.of_fintype le_top
smithNormalFormBotBasis_def 📖	mathematical	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike addCommMonoid module	DFunLike.coe Module.Basis Module.Basis.instFunLike smithNormalFormBotBasis SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smithNormalFormCoeffs smithNormalFormTopBasis	—	exists_smith_normal_form_of_rank_eq
smithNormalFormCoeffs_ne_zero 📖	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike addCommMonoid module	—	—	Module.Basis.ne_zero IsDomain.toNontrivial Subtype.coe_injective smithNormalFormBotBasis_def zero_smul

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_generator_iff 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring Submodule.IsPrincipal.generator Ideal.span Set Set.instSingletonSet	—	Ideal.span_singleton_le_iff_mem Submodule.IsPrincipal.span_singleton_generator Submodule.span_singleton_le_iff_mem
eq_bot_of_generator_maximal_map_eq_zero 📖	mathematical	Submodule Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semiring.toModule Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder Submodule.map AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Submodule.IsPrincipal.generator MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Bot.bot Submodule.instBot	—	RingHomSurjective.ids Submodule.eq_bot_iff Module.Basis.ext_elem RingHomInvPair.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finsupp.zero_apply RingHomCompTriple.ids not_bot_lt_iff Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero
eq_bot_of_generator_maximal_submoduleImage_eq_zero 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semiring.toModule Preorder.toLT LinearMap.submoduleImage Submodule.IsPrincipal.generator MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Bot.bot Submodule.instBot	—	Submodule.eq_bot_iff Submodule.mk_eq_zero Module.Basis.ext_elem RingHomInvPair.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finsupp.zero_apply RingHomCompTriple.ids not_bot_lt_iff Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero LinearMap.mem_submoduleImage_of_le
generator_maximal_submoduleImage_dvd 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Preorder.toLT LinearMap.submoduleImage SetLike.instMembership Submodule.setLike DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid Submodule.module LinearMap.instFunLike Submodule.IsPrincipal.generator	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring	—	IsPrincipalIdealRing.principal Submodule.IsPrincipal.mem_iff_generator_dvd Submodule.subset_span Set.mem_insert Set.mem_insert_of_mem Set.mem_singleton dvd_trans dvd_generator_iff Ideal.span.eq_1 Submodule.IsPrincipal.span_singleton_generator Submodule.mem_span_insert Submodule.IsPrincipal.generator_mem Submodule.mem_span_singleton Algebra.to_smulCommClass Submodule.span_le Set.singleton_subset_iff SetLike.mem_coe LinearMap.mem_submoduleImage_of_le le_antisymm LE.le.trans le_of_eq LE.le.eq_of_not_lt' le_trans Ideal.span_singleton_le_span_singleton
instFreeSubtypeMemIdealOfFiniteOfIsTorsionFree 📖	mathematical	—	Module.Free Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.addCommMonoid Submodule.module' Algebra.toSMul Algebra.toModule IsScalarTower.right	—	IsScalarTower.right Module.free_of_finite_type_torsion_free'

---

← Back to Index