# Torsion submodules #

## Main definitions #

• torsionOf R M x : the torsion ideal of x, containing all a such that a • x = 0.
• Submodule.torsionBy R M a : the a-torsion submodule, containing all elements x of M such that a • x = 0.
• Submodule.torsionBySet R M s : the submodule containing all elements x of M such that a • x = 0 for all a in s.
• Submodule.torsion' R M S : the S-torsion submodule, containing all elements x of M such that a • x = 0 for some a in S.
• Submodule.torsion R M : the torsion submodule, containing all elements x of M such that a • x = 0 for some non-zero-divisor a in R.
• Module.IsTorsionBy R M a : the property that defines an a-torsion module. Similarly, IsTorsionBySet, IsTorsion' and IsTorsion.
• Module.IsTorsionBySet.module : Creates an R ⧸ I-module from an R-module that IsTorsionBySet R _ I.

## Main statements #

• quot_torsionOf_equiv_span_singleton : isomorphism between the span of an element of M and the quotient by its torsion ideal.
• torsion' R M S and torsion R M are submodules.
• torsionBySet_eq_torsionBySet_span : torsion by a set is torsion by the ideal generated by it.
• Submodule.torsionBy_is_torsionBy : the a-torsion submodule is an a-torsion module. Similar lemmas for torsion' and torsion.
• Submodule.torsionBy_isInternal : a ∏ i, p i-torsion module is the internal direct sum of its p i-torsion submodules when the p i are pairwise coprime. A more general version with coprime ideals is Submodule.torsionBySet_is_internal.
• Submodule.noZeroSMulDivisors_iff_torsion_bot : a module over a domain has NoZeroSMulDivisors (that is, there is no non-zero a, x such that a • x = 0) iff its torsion submodule is trivial.
• Submodule.QuotientTorsion.torsion_eq_bot : quotienting by the torsion submodule makes the torsion submodule of the new module trivial. If R is a domain, we can derive an instance Submodule.QuotientTorsion.noZeroSMulDivisors : NoZeroSMulDivisors R (M ⧸ torsion R M).

## Notation #

• The notions are defined for a CommSemiring R and a Module R M. Some additional hypotheses on R and M are required by some lemmas.
• The letters a, b, ... are used for scalars (in R), while x, y, ... are used for vectors (in M).

## Tags #

Torsion, submodule, module, quotient

@[simp]
theorem Ideal.torsionOf_carrier (R : Type u_1) (M : Type u_2) [] [] [Module R M] (x : M) :
() = () ⁻¹' {0}
def Ideal.torsionOf (R : Type u_1) (M : Type u_2) [] [] [Module R M] (x : M) :

The torsion ideal of x, containing all a such that a • x = 0.

Equations
Instances For
@[simp]
theorem Ideal.torsionOf_zero (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
@[simp]
theorem Ideal.mem_torsionOf_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] (x : M) (a : R) :
a a x = 0
@[simp]
theorem Ideal.torsionOf_eq_top_iff (R : Type u_1) {M : Type u_2} [] [] [Module R M] (m : M) :
= m = 0
@[simp]
theorem Ideal.torsionOf_eq_bot_iff_of_noZeroSMulDivisors (R : Type u_1) {M : Type u_2} [] [] [Module R M] [] [] (m : M) :
= m 0
theorem Ideal.CompleteLattice.Independent.linear_independent' {ι : Type u_3} {R : Type u_4} {M : Type u_5} {v : ιM} [Ring R] [] [Module R M] (hv : CompleteLattice.Independent fun (i : ι) => Submodule.span R {v i}) (h_ne_zero : ∀ (i : ι), Ideal.torsionOf R M (v i) = ) :

See also CompleteLattice.Independent.linearIndependent which provides the same conclusion but requires the stronger hypothesis NoZeroSMulDivisors R M.

noncomputable def Ideal.quotTorsionOfEquivSpanSingleton (R : Type u_1) (M : Type u_2) [Ring R] [] [Module R M] (x : M) :
(R ) ≃ₗ[R] (Submodule.span R {x})

The span of x in M is isomorphic to R quotiented by the torsion ideal of x.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Ideal.quotTorsionOfEquivSpanSingleton_apply_mk {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (x : M) (a : R) :
= a x,
@[simp]
theorem Submodule.torsionBy_carrier (R : Type u_1) (M : Type u_2) [] [] [Module R M] (a : R) :
() = () ⁻¹' {0}
def Submodule.torsionBy (R : Type u_1) (M : Type u_2) [] [] [Module R M] (a : R) :

The a-torsion submodule for a in R, containing all elements x of M such that a • x = 0.

Equations
Instances For
@[simp]
theorem Submodule.torsionBySet_carrier (R : Type u_1) (M : Type u_2) [] [] [Module R M] (s : Set R) :
() = ys, () ⁻¹' {0}
def Submodule.torsionBySet (R : Type u_1) (M : Type u_2) [] [] [Module R M] (s : Set R) :

The submodule containing all elements x of M such that a • x = 0 for all a in s.

Equations
Instances For
@[simp]
theorem Submodule.torsion'AddSubMonoid_coe (M : Type u_2) [] (S : Type u_3) [] [] :
= {x : M | ∃ (a : S), a x = 0}
def Submodule.torsion'AddSubMonoid (M : Type u_2) [] (S : Type u_3) [] [] :

The additive submonoid of all elements x of M such that a • x = 0 for some a in S.

Equations
• = { carrier := {x : M | ∃ (a : S), a x = 0}, add_mem' := , zero_mem' := }
Instances For
@[simp]
theorem Submodule.torsion'_carrier (R : Type u_1) (M : Type u_2) [] [] [Module R M] (S : Type u_3) [] [] [] :
() = {x : M | ∃ (a : S), a x = 0}
def Submodule.torsion' (R : Type u_1) (M : Type u_2) [] [] [Module R M] (S : Type u_3) [] [] [] :

The S-torsion submodule, containing all elements x of M such that a • x = 0 for some a in S.

Equations
• = let __src := ; { toAddSubmonoid := __src, smul_mem' := }
Instances For
@[reducible, inline]
abbrev Submodule.torsion (R : Type u_1) (M : Type u_2) [] [] [Module R M] :

The torsion submodule, containing all elements x of M such that a • x = 0 for some non-zero-divisor a in R.

Equations
Instances For
@[reducible, inline]
abbrev Module.IsTorsionBy (R : Type u_1) (M : Type u_2) [] [] [Module R M] (a : R) :

An a-torsion module is a module where every element is a-torsion.

Equations
• = ∀ ⦃x : M⦄, a x = 0
Instances For
@[reducible, inline]
abbrev Module.IsTorsionBySet (R : Type u_1) (M : Type u_2) [] [] [Module R M] (s : Set R) :

A module where every element is a-torsion for all a in s.

Equations
• = ∀ ⦃x : M⦄ ⦃a : s⦄, a x = 0
Instances For
@[reducible, inline]
abbrev Module.IsTorsion' (M : Type u_2) [] (S : Type u_3) [SMul S M] :

An S-torsion module is a module where every element is a-torsion for some a in S.

Equations
• = ∀ ⦃x : M⦄, ∃ (a : S), a x = 0
Instances For
@[reducible, inline]
abbrev Module.IsTorsion (R : Type u_1) (M : Type u_2) [] [] [Module R M] :

A torsion module is a module where every element is a-torsion for some non-zero-divisor a.

Equations
• = ∀ ⦃x : M⦄, ∃ (a : ()), a x = 0
Instances For
theorem Module.isTorsionBySet_annihilator (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
theorem isSMulRegular_iff_torsionBy_eq_bot {R : Type u_2} (M : Type u_1) [] [] [Module R M] (r : R) :
@[simp]
theorem Submodule.smul_torsionBy {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) (x : ()) :
a x = 0
@[simp]
theorem Submodule.smul_coe_torsionBy {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) (x : ()) :
a x = 0
@[simp]
theorem Submodule.mem_torsionBy_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) (x : M) :
x a x = 0
@[simp]
theorem Submodule.mem_torsionBySet_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] (s : Set R) (x : M) :
x ∀ (a : s), a x = 0
@[simp]
theorem Submodule.torsionBySet_singleton_eq {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) :
=
theorem Submodule.torsionBySet_le_torsionBySet_of_subset {R : Type u_1} {M : Type u_2} [] [] [Module R M] {s : Set R} {t : Set R} (st : s t) :
theorem Submodule.torsionBySet_eq_torsionBySet_span {R : Type u_1} {M : Type u_2} [] [] [Module R M] (s : Set R) :
=

Torsion by a set is torsion by the ideal generated by it.

theorem Submodule.torsionBySet_span_singleton_eq {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) :
theorem Submodule.torsionBy_le_torsionBy_of_dvd {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) (b : R) (dvd : a b) :
@[simp]
theorem Submodule.torsionBy_one {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
@[simp]
theorem Submodule.torsionBySet_univ {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
@[simp]
theorem Module.isTorsionBySet_singleton_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) :
theorem Module.isTorsionBySet_iff_torsionBySet_eq_top {R : Type u_1} {M : Type u_2} [] [] [Module R M] (s : Set R) :
theorem Module.isTorsionBy_iff_torsionBy_eq_top {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) :

An a-torsion module is a module whose a-torsion submodule is the full space.

theorem Module.isTorsionBySet_iff_is_torsion_by_span {R : Type u_1} {M : Type u_2} [] [] [Module R M] (s : Set R) :
theorem Module.isTorsionBySet_span_singleton_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) :
theorem Module.isTorsionBySet_iff_subseteq_ker_lsmul {R : Type u_1} {M : Type u_2} [] [] [Module R M] (s : Set R) :
s ()
theorem Module.isTorsionBy_iff_mem_ker_lsmul {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) :
a
theorem Submodule.torsionBySet_isTorsionBySet {R : Type u_1} {M : Type u_2} [] [] [Module R M] (s : Set R) :
theorem Submodule.torsionBy_isTorsionBy {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) :
Module.IsTorsionBy R (()) a

The a-torsion submodule is an a-torsion module.

@[simp]
theorem Submodule.torsionBy_torsionBy_eq_top {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) :
@[simp]
theorem Submodule.torsionBySet_torsionBySet_eq_top {R : Type u_1} {M : Type u_2} [] [] [Module R M] (s : Set R) :
theorem Submodule.torsion_gc (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
GaloisConnection Submodule.annihilator fun (I : ()ᵒᵈ) => Submodule.torsionBySet R M (OrderDual.ofDual I)
theorem Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ι : Type u_3} {p : ι} {S : } (hp : (S).Pairwise fun (i j : ι) => p i p j = ) :
iS, Submodule.torsionBySet R M (p i) = Submodule.torsionBySet R M (iS, p i)
theorem Submodule.supIndep_torsionBySet_ideal {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ι : Type u_3} {p : ι} {S : } (hp : (S).Pairwise fun (i j : ι) => p i p j = ) :
S.SupIndep fun (i : ι) => Submodule.torsionBySet R M (p i)
theorem Submodule.iSup_torsionBy_eq_torsionBy_prod {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ι : Type u_3} {S : } {q : ιR} (hq : (S).Pairwise (IsCoprime on q)) :
iS, Submodule.torsionBy R M (q i) = Submodule.torsionBy R M (S.prod fun (i : ι) => q i)
theorem Submodule.supIndep_torsionBy {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ι : Type u_3} {S : } {q : ιR} (hq : (S).Pairwise (IsCoprime on q)) :
S.SupIndep fun (i : ι) => Submodule.torsionBy R M (q i)
theorem Submodule.torsionBySet_isInternal {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ι : Type u_3} [] {S : } {p : ι} (hp : (S).Pairwise fun (i j : ι) => p i p j = ) (hM : Module.IsTorsionBySet R M (iS, p i)) :
DirectSum.IsInternal fun (i : { x : ι // x S }) => Submodule.torsionBySet R M (p i)

If the p i are pairwise coprime, a ⨅ i, p i-torsion module is the internal direct sum of its p i-torsion submodules.

theorem Submodule.torsionBy_isInternal {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ι : Type u_3} [] {S : } {q : ιR} (hq : (S).Pairwise (IsCoprime on q)) (hM : Module.IsTorsionBy R M (S.prod fun (i : ι) => q i)) :
DirectSum.IsInternal fun (i : { x : ι // x S }) => Submodule.torsionBy R M (q i)

If the q i are pairwise coprime, a ∏ i, q i-torsion module is the internal direct sum of its q i-torsion submodules.

def Module.IsTorsionBySet.hasSMul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {I : } (hM : ) :
SMul (R I) M

can't be an instance because hM can't be inferred

Equations
Instances For
@[reducible, inline]
abbrev Module.IsTorsionBy.hasSMul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {r : R} (hM : ) :
SMul (R Ideal.span {r}) M

can't be an instance because hM can't be inferred

Equations
• hM.hasSMul = .hasSMul
Instances For
@[simp]
theorem Module.IsTorsionBySet.mk_smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {I : } (hM : ) (b : R) (x : M) :
b x = b x
@[simp]
theorem Module.IsTorsionBy.mk_smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {r : R} (hM : ) (b : R) (x : M) :
() b x = b x
def Module.IsTorsionBySet.module {R : Type u_1} {M : Type u_2} [] [] [Module R M] {I : } (hM : ) :
Module (R I) M

An (R ⧸ I)-module is an R-module which IsTorsionBySet R M I.

Equations
• hM.module =
Instances For
instance Module.IsTorsionBySet.isScalarTower {R : Type u_1} {M : Type u_2} [] [] [Module R M] {I : } (hM : ) {S : Type u_3} [SMul S R] [SMul S M] [] [] :
IsScalarTower S (R I) M
Equations
• =
@[reducible, inline]
abbrev Module.IsTorsionBy.module {R : Type u_1} {M : Type u_2} [] [] [Module R M] {r : R} (hM : ) :

An (R ⧸ Ideal.span {r})-module is an R-module for which IsTorsionBy R M r.

Equations
• hM.module = .module
Instances For
def Module.quotientAnnihilator {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
Module (R ) M

Any module is also a module over the quotient of the ring by the annihilator. Not an instance because it causes synthesis failures / timeouts.

Equations
• Module.quotientAnnihilator = .module
Instances For
theorem Module.isTorsionBy_quotient_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] (N : ) (r : R) :
Module.IsTorsionBy R (M N) r ∀ (x : M), r x N
theorem Module.IsTorsionBy.quotient {R : Type u_1} {M : Type u_2} [] [] [Module R M] (N : ) {r : R} (h : ) :
theorem Module.isTorsionBySet_quotient_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] (N : ) (s : Set R) :
Module.IsTorsionBySet R (M N) s ∀ (x : M), rs, r x N
theorem Module.IsTorsionBySet.quotient {R : Type u_1} {M : Type u_2} [] [] [Module R M] (N : ) {s : Set R} (h : ) :
theorem Module.isTorsionBySet_quotient_set_smul {R : Type u_1} (M : Type u_2) [] [] [Module R M] (s : Set R) :
theorem Module.isTorsionBy_quotient_element_smul {R : Type u_1} (M : Type u_2) [] [] [Module R M] (r : R) :
theorem Module.isTorsionBySet_quotient_ideal_smul {R : Type u_1} (M : Type u_2) [] [] [Module R M] (I : ) :
instance Module.instQuotientIdealSpanSubmoduleHSMulSetTop {R : Type u_1} (M : Type u_2) [] [] [Module R M] (s : Set R) :
Module (R ) (M s )
Equations
instance Module.instQuotientIdealSubmoduleHSMulTop {R : Type u_1} (M : Type u_2) [] [] [Module R M] (I : ) :
Module (R I) (M I )
Equations
• = .module
instance Module.instQuotientIdealSpanSingletonSetSubmoduleHSMulTop {R : Type u_1} (M : Type u_2) [] [] [Module R M] (r : R) :
Module (R Ideal.span {r}) (M r )
Equations
theorem Module.Quotient.mk_smul_mk {R : Type u_1} (M : Type u_2) [] [] [Module R M] (I : ) (r : R) (m : M) :
instance Submodule.instModuleQuotientIdealSubtypeMemTorsionBySetCoe {R : Type u_1} {M : Type u_2} [] [] [Module R M] (I : ) :
Module (R I) ()
Equations
@[simp]
theorem Submodule.torsionBySet.mk_smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] (I : ) (b : R) (x : ()) :
b x = b x
instance Submodule.instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe {R : Type u_1} {M : Type u_2} [] [] [Module R M] (I : ) {S : Type u_3} [SMul S R] [SMul S M] [] [] :
IsScalarTower S (R I) ()
Equations
• =
instance Submodule.instModuleQuotientTorsionBy {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) :
Module (R Submodule.span R {a}) ()

The a-torsion submodule as an (R ⧸ R∙a)-module.

Equations
• = .module
instance Submodule.instModuleQuotientIdealSpanSingletonSetSubtypeMemTorsionBy {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) :
Module (R Ideal.span {a}) ()
Equations
@[simp]
theorem Submodule.torsionBy.mk_ideal_smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) (b : R) (x : ()) :
() b x = b x
theorem Submodule.torsionBy.mk_smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) (b : R) (x : ()) :
instance Submodule.instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) {S : Type u_3} [SMul S R] [SMul S M] [] [] :
IsScalarTower S (R Submodule.span R {a}) ()
Equations
• =
def Submodule.submodule_torsionBy_orderIso {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : R) :
Submodule (R Submodule.span R {a}) () ≃o Submodule R ()

Given an R-module M and an element a in R, submodules of the a-torsion submodule of M do not depend on whether we take scalars to be R or R ⧸ R ∙ a.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Submodule.mem_torsion'_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] (S : Type u_3) [] [] [] (x : M) :
x ∃ (a : S), a x = 0
theorem Submodule.mem_torsion_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] (x : M) :
x ∃ (a : ()), a x = 0
@[simp]
theorem Submodule.instSMulSubtypeMemTorsion'_smul_coe {R : Type u_1} {M : Type u_2} [] [] [Module R M] (S : Type u_3) [] [] [] (s : S) (x : ()) :
(s x) = s x
instance Submodule.instSMulSubtypeMemTorsion' {R : Type u_1} {M : Type u_2} [] [] [Module R M] (S : Type u_3) [] [] [] :
SMul S ()
Equations
• = { smul := fun (s : S) (x : ()) => s x, }
instance Submodule.instDistribMulActionSubtypeMemTorsion' {R : Type u_1} {M : Type u_2} [] [] [Module R M] (S : Type u_3) [] [] [] :
Equations
instance Submodule.instSMulCommClassSubtypeMemTorsion' {R : Type u_1} {M : Type u_2} [] [] [Module R M] (S : Type u_3) [] [] [] :
SMulCommClass S R ()
Equations
• =
theorem Submodule.isTorsion'_iff_torsion'_eq_top {R : Type u_1} {M : Type u_2} [] [] [Module R M] (S : Type u_3) [] [] [] :

An S-torsion module is a module whose S-torsion submodule is the full space.

theorem Submodule.torsion'_isTorsion' {R : Type u_1} {M : Type u_2} [] [] [Module R M] (S : Type u_3) [] [] [] :

The S-torsion submodule is an S-torsion module.

@[simp]
theorem Submodule.torsion'_torsion'_eq_top {R : Type u_1} {M : Type u_2} [] [] [Module R M] (S : Type u_3) [] [] [] :
theorem Submodule.torsion_torsion_eq_top {R : Type u_1} {M : Type u_2} [] [] [Module R M] :

The torsion submodule of the torsion submodule (viewed as a module) is the full torsion module.

theorem Submodule.torsion_isTorsion {R : Type u_1} {M : Type u_2} [] [] [Module R M] :

The torsion submodule is always a torsion module.

theorem Module.isTorsionBySet_annihilator_top (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
Module.IsTorsionBySet R M .annihilator
theorem Submodule.annihilator_top_inter_nonZeroDivisors {R : Type u_1} {M : Type u_2} [] [] [Module R M] [] (hM : ) :
.annihilator ()
theorem Submodule.coe_torsion_eq_annihilator_ne_bot {R : Type u_1} {M : Type u_2} [] [] [Module R M] [] [] :
() = {x : M | (Submodule.span R {x}).annihilator }
theorem Submodule.noZeroSMulDivisors_iff_torsion_eq_bot {R : Type u_1} {M : Type u_2} [] [] [Module R M] [] [] :

A module over a domain has NoZeroSMulDivisors iff its torsion submodule is trivial.

theorem Submodule.torsion_int {G : Type u_3} [] :
@[simp]
theorem Submodule.QuotientTorsion.torsion_eq_bot {R : Type u_1} {M : Type u_2} [] [] [Module R M] :

Quotienting by the torsion submodule gives a torsion-free module.

instance Submodule.QuotientTorsion.noZeroSMulDivisors {R : Type u_1} {M : Type u_2} [] [] [Module R M] [] :
Equations
• =
theorem Submodule.isTorsion'_powers_iff {R : Type u_1} {M : Type u_2} [] [] [] (p : R) :
∀ (x : M), ∃ (n : ), p ^ n x = 0
def Submodule.pOrder {R : Type u_1} {M : Type u_2} [] [] [] {p : R} (hM : ) (x : M) [(n : ) → Decidable (p ^ n x = 0)] :

In a p ^ ∞-torsion module (that is, a module where all elements are cancelled by scalar multiplication by some power of p), the smallest n such that p ^ n • x = 0.

Equations
Instances For
@[simp]
theorem Submodule.pow_pOrder_smul {R : Type u_1} {M : Type u_2} [] [] [] {p : R} (hM : ) (x : M) [(n : ) → Decidable (p ^ n x = 0)] :
p ^ x = 0
theorem Submodule.exists_isTorsionBy {R : Type u_1} {M : Type u_2} [] [] [Module R M] [(x : M) → Decidable (x = 0)] {p : R} (hM : ) (d : ) (hd : d 0) (s : Fin dM) (hs : = ) :
∃ (j : Fin d), Module.IsTorsionBy R M (p ^ Submodule.pOrder hM (s j))