Documentation

Mathlib.Algebra.Module.Torsion

Torsion submodules #

Main definitions #

Main statements #

Notation #

Tags #

Torsion, submodule, module, quotient

def Ideal.torsionOf (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :

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

Equations
@[simp]
theorem Ideal.coe_torsionOf (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
@[simp]
theorem Ideal.torsionOf_zero (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] :
@[simp]
theorem Ideal.mem_torsionOf_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) (a : R) :
a torsionOf R M x a x = 0
@[simp]
theorem Ideal.torsionOf_eq_top_iff (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (m : M) :
torsionOf R M m = m = 0
@[simp]
theorem Ideal.iSupIndep.linearIndependent' {ι : Type u_3} {R : Type u_4} {M : Type u_5} {v : ιM} [Ring R] [AddCommGroup M] [Module R M] (hv : iSupIndep fun (i : ι) => Submodule.span R {v i}) (h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ) :

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

@[deprecated Ideal.iSupIndep.linearIndependent' (since := "2024-11-24")]
theorem Ideal.CompleteLattice.Independent.linear_independent' {ι : Type u_3} {R : Type u_4} {M : Type u_5} {v : ιM} [Ring R] [AddCommGroup M] [Module R M] (hv : iSupIndep fun (i : ι) => Submodule.span R {v i}) (h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ) :

Alias of Ideal.iSupIndep.linearIndependent'.


See also iSupIndep.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] [AddCommGroup M] [Module R M] (x : M) :

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.
@[simp]
theorem Ideal.quotTorsionOfEquivSpanSingleton_apply_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (x : M) (a : R) :
def Submodule.torsionBy (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [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
@[simp]
theorem Submodule.coe_torsionBy (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) :
def Submodule.torsionBySet (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [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
@[simp]
theorem Submodule.coe_torsionBySet (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) :
(torsionBySet R M s) = ys, (DistribMulAction.toLinearMap R M y) ⁻¹' {0}

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

Equations
@[simp]
theorem Submodule.coe_torsion'AddSubMonoid (M : Type u_2) [AddCommMonoid M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] :
(torsion'AddSubMonoid M S) = {x : M | ∃ (a : S), a x = 0}
def Submodule.torsion' (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] :

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

Equations
@[simp]
theorem Submodule.coe_torsion' (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] :
(torsion' R M S) = {x : M | ∃ (a : S), a x = 0}
@[reducible, inline]
abbrev Submodule.torsion (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [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
@[reducible, inline]
abbrev Module.IsTorsionBy (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (a : R) :

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

Equations
@[reducible, inline]
abbrev Module.IsTorsionBySet (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set R) :

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

Equations
@[reducible, inline]
abbrev Module.IsTorsion' (M : Type u_2) [AddCommMonoid M] (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
@[reducible, inline]
abbrev Module.IsTorsion (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] :

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

Equations
theorem Module.isTorsionBy_iff_mem_annihilator (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] {a : R} :
@[simp]
theorem Submodule.smul_torsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) (x : (torsionBy R M a)) :
a x = 0
@[simp]
theorem Submodule.smul_coe_torsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) (x : (torsionBy R M a)) :
a x = 0
@[simp]
theorem Submodule.mem_torsionBy_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) (x : M) :
x torsionBy R M a a x = 0
@[simp]
theorem Submodule.mem_torsionBySet_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (x : M) :
x torsionBySet R M s ∀ (a : s), a x = 0
@[simp]
theorem Submodule.torsionBySet_singleton_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) :
theorem Submodule.torsionBySet_le_torsionBySet_of_subset {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {s t : Set R} (st : s t) :

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} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) :
torsionBySet R M (span R {a}) = torsionBy R M a
theorem Submodule.torsionBy_le_torsionBy_of_dvd {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a b : R) (dvd : a b) :
torsionBy R M a torsionBy R M b
@[simp]
theorem Submodule.torsionBy_one {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
@[simp]
theorem Module.isTorsionBySet_of_subset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set R} (h : s t) (ht : IsTorsionBySet R M t) :
@[simp]
theorem Module.isTorsionBySet_singleton_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (a : R) :

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

theorem Submodule.torsionBy_isTorsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) :
Module.IsTorsionBy R (↥(torsionBy R M a)) 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} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) :
torsionBy R (↥(torsionBy R M a)) a =
@[simp]
theorem Submodule.torsionBySet_torsionBySet_eq_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) :
torsionBySet R (↥(torsionBySet R M s)) s =
theorem Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {p : ιIdeal R} {S : Finset ι} (hp : (↑S).Pairwise fun (i j : ι) => p i p j = ) :
iS, torsionBySet R M (p i) = torsionBySet R M (⨅ iS, p i)
theorem Submodule.supIndep_torsionBySet_ideal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {p : ιIdeal R} {S : Finset ι} (hp : (↑S).Pairwise fun (i j : ι) => p i p j = ) :
S.SupIndep fun (i : ι) => torsionBySet R M (p i)
theorem Submodule.iSup_torsionBy_eq_torsionBy_prod {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {S : Finset ι} {q : ιR} (hq : (↑S).Pairwise (Function.onFun IsCoprime q)) :
iS, torsionBy R M (q i) = torsionBy R M (∏ iS, q i)
theorem Submodule.supIndep_torsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {S : Finset ι} {q : ιR} (hq : (↑S).Pairwise (Function.onFun IsCoprime q)) :
S.SupIndep fun (i : ι) => torsionBy R M (q i)
theorem Submodule.torsionBySet_isInternal {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [DecidableEq ι] {S : Finset ι} {p : ιIdeal R} (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 }) => 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} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [DecidableEq ι] {S : Finset ι} {q : ιR} (hq : (↑S).Pairwise (Function.onFun IsCoprime q)) (hM : Module.IsTorsionBy R M (∏ iS, q i)) :
DirectSum.IsInternal fun (i : { x : ι // x S }) => 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} [Ring R] [AddCommGroup M] [Module R M] {I : Ideal R} (hM : IsTorsionBySet R M I) :
SMul (R I) M

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

Equations
@[reducible, inline]
abbrev Module.IsTorsionBy.hasSMul {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {r : R} (hM : IsTorsionBy R M r) :

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

Equations
@[simp]
theorem Module.IsTorsionBySet.mk_smul {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {I : Ideal R} [I.IsTwoSided] (hM : IsTorsionBySet R M I) (b : R) (x : M) :
@[simp]
theorem Module.IsTorsionBy.mk_smul {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {r : R} [(Ideal.span {r}).IsTwoSided] (hM : IsTorsionBy R M r) (b : R) (x : M) :
def Module.IsTorsionBySet.module {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {I : Ideal R} [I.IsTwoSided] (hM : IsTorsionBySet R M I) :
Module (R I) M

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

Equations
instance Module.IsTorsionBySet.isScalarTower {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {I : Ideal R} [I.IsTwoSided] (hM : IsTorsionBySet R M I) {S : Type u_3} [SMul S R] [SMul S M] [IsScalarTower S R M] [IsScalarTower S R R] :
IsScalarTower S (R I) M
def Module.IsTorsionBySet.semilinearMap {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {I : Ideal R} [I.IsTwoSided] (hM : IsTorsionBySet R M I) :

If a R-module M is annihilated by a two-sided ideal I, then the identity is a semilinear map from the R-module M to the R ⧸ I-module M.

Equations
@[reducible, inline]
abbrev Module.IsTorsionBy.module {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {r : R} [h : (Ideal.span {r}).IsTwoSided] (hM : IsTorsionBy R M r) :

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

Equations
def Module.quotientAnnihilator {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup 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
theorem Module.isTorsionBy_quotient_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) (r : R) :
IsTorsionBy R (M N) r ∀ (x : M), r x N
theorem Module.IsTorsionBy.quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) {r : R} (h : IsTorsionBy R M r) :
IsTorsionBy R (M N) r
theorem Module.isTorsionBySet_quotient_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) (s : Set R) :
IsTorsionBySet R (M N) s ∀ (x : M), rs, r x N
theorem Module.IsTorsionBySet.quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) {s : Set R} (h : IsTorsionBySet R M s) :
theorem Module.isTorsionBySet_quotient_set_smul {R : Type u_1} (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] (s : Set R) :
theorem Module.isTorsionBySet_quotient_ideal_smul {R : Type u_1} (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] (I : Ideal R) :
IsTorsionBySet R (M I ) I
theorem Module.Quotient.mk_smul_mk {R : Type u_1} (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] (I : Ideal R) [I.IsTwoSided] (r : R) (m : M) :
theorem Module.isTorsionBy_quotient_element_smul {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (r : R) :
@[simp]
theorem Submodule.torsionBySet.mk_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (b : R) (x : (torsionBySet R M I)) :
instance Submodule.instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) {S : Type u_3} [SMul S R] [SMul S M] [IsScalarTower S R M] [IsScalarTower S R R] :
IsScalarTower S (R I) (torsionBySet R M I)
instance Submodule.instModuleQuotientTorsionBy {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a : R) :
Module (R span R {a}) (torsionBy R M a)

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

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

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.
@[simp]
theorem Submodule.mem_torsion'_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] (x : M) :
x torsion' R M S ∃ (a : S), a x = 0
theorem Submodule.mem_torsion_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : M) :
x torsion R M ∃ (a : (nonZeroDivisors R)), a x = 0
instance Submodule.instSMulSubtypeMemTorsion' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] :
SMul S (torsion' R M S)
Equations
@[simp]
theorem Submodule.instSMulSubtypeMemTorsion'_smul_coe {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) (x : (torsion' R M S)) :
↑(s x) = s x

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} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] :

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

@[simp]
theorem Submodule.torsion'_torsion'_eq_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] :
torsion' R (↥(torsion' R M S)) S =
theorem Submodule.torsion_torsion_eq_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :
torsion R (torsion 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} [CommSemiring R] [AddCommMonoid M] [Module R M] :

The torsion submodule is always a torsion module.

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

@[simp]

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

theorem Submodule.isTorsion'_powers_iff {R : Type u_1} {M : Type u_2} [Monoid R] [AddCommMonoid M] [DistribMulAction R M] (p : R) :
Module.IsTorsion' M (Submonoid.powers p) ∀ (x : M), ∃ (n : ), p ^ n x = 0
def Submodule.pOrder {R : Type u_1} {M : Type u_2} [Monoid R] [AddCommMonoid M] [DistribMulAction R M] {p : R} (hM : Module.IsTorsion' M (Submonoid.powers p)) (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
@[simp]
theorem Submodule.pow_pOrder_smul {R : Type u_1} {M : Type u_2} [Monoid R] [AddCommMonoid M] [DistribMulAction R M] {p : R} (hM : Module.IsTorsion' M (Submonoid.powers p)) (x : M) [(n : ) → Decidable (p ^ n x = 0)] :
p ^ pOrder hM x x = 0
theorem Submodule.exists_isTorsionBy {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [(x : M) → Decidable (x = 0)] {p : R} (hM : Module.IsTorsion' M (Submonoid.powers p)) (d : ) (hd : d 0) (s : Fin dM) (hs : span R (Set.range s) = ) :
∃ (j : Fin d), Module.IsTorsionBy R M (p ^ pOrder hM (s j))
@[reducible]

The additive n-torsion subgroup for an integer n, denoted as A[n].

Equations

The additive n-torsion subgroup for an integer n, denoted as A[n].

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubgroup.torsionBy.nsmul {A : Type u_3} [AddCommGroup A] {n : } (x : (torsionBy A n)) :
n x = 0
theorem AddSubgroup.torsionBy.nsmul_iff {A : Type u_3} [AddCommGroup A] {n : } {x : A} :
x torsionBy A n n x = 0
theorem AddSubgroup.torsionBy.mod_self_nsmul {A : Type u_3} [AddCommGroup A] {n : } (s : ) (x : (torsionBy A n)) :
s x = (s % n) x
theorem AddSubgroup.torsionBy.mod_self_nsmul' {A : Type u_3} [AddCommGroup A] {n : } (s : ) {x : A} (h : x torsionBy A n) :
s x = (s % n) x
def AddSubgroup.torsionBy.zmodModule {A : Type u_3} [AddCommGroup A] {n : } :
Module (ZMod n) (torsionBy A n)

For a natural number n, the n-torsion subgroup of A is a ZMod n module.

Equations
@[simp]
theorem infinite_range_add_smul_iff {R : Type u_1} {M : Type u_2} [AddCommGroup M] [Ring R] [Module R M] [Infinite R] [NoZeroSMulDivisors R M] (x y : M) :
(Set.range fun (r : R) => x + r y).Infinite y 0
@[simp]
theorem infinite_range_add_nsmul_iff {M : Type u_2} [AddCommGroup M] [NoZeroSMulDivisors M] (x y : M) :
(Set.range fun (n : ) => x + n y).Infinite y 0