Mathlib.LinearAlgebra.Basis.Basic

Basis.repr_range theorem

: LinearMap.range (b.repr : M →ₗ[R] ι →₀ R) = Finsupp.supported R R univ

Full source

theorem repr_range : LinearMap.range (b.repr : M →ₗ[R] ι →₀ R) = Finsupp.supported R R univ := by
  rw [LinearEquiv.range, Finsupp.supported_univ]

Range of Basis Representation Equals Full Support Functions

Informal description

For a basis $b$ of a module $M$ over a ring $R$ indexed by $\iota$, the range of the representation map $b.\text{repr} : M \to \iota \to_{\text{f}} R$ is equal to the set of all finitely supported functions from $\iota$ to $R$ with full support, i.e., $\text{range}(b.\text{repr}) = \{f : \iota \to_{\text{f}} R \mid \text{support}(f) = \text{univ}\}$.

Basis.mem_span_repr_support theorem

(m : M) : m ∈ span R (b '' (b.repr m).support)

Full source

theorem mem_span_repr_support (m : M) : m ∈ span R (b '' (b.repr m).support) :=
  (Finsupp.mem_span_image_iff_linearCombination _).2
    ⟨b.repr m, by simp [Finsupp.mem_supported_support]⟩

Vector Lies in Span of Basis Vectors Corresponding to Nonzero Coordinates

Informal description

For any vector $m$ in a module $M$ with basis $b$ over a ring $R$, the vector $m$ lies in the span of the basis vectors indexed by the support of its coordinate representation. That is, $m \in \text{span}_R \{b(i) \mid i \in \text{supp}(b.\text{repr}(m))\}$.

Basis.repr_support_subset_of_mem_span theorem

(s : Set ι) {m : M} (hm : m ∈ span R (b '' s)) : ↑(b.repr m).support ⊆ s

Full source

theorem repr_support_subset_of_mem_span (s : Set ι) {m : M}
    (hm : m ∈ span R (b '' s)) : ↑(b.repr m).support ⊆ s := by
  rcases (Finsupp.mem_span_image_iff_linearCombination _).1 hm with ⟨l, hl, rfl⟩
  rwa [repr_linearCombination, ← Finsupp.mem_supported R l]

Support of Coordinates in Span of Basis Subset

Informal description

Let $M$ be a module over a ring $R$ with basis $b$ indexed by a set $\iota$, and let $s \subseteq \iota$. For any element $m \in M$ that lies in the span of the basis vectors $\{b(i) \mid i \in s\}$, the support of the coordinate representation $b.\text{repr}(m)$ is contained in $s$. That is: $$ \text{support}(b.\text{repr}(m)) \subseteq s $$

Basis.mem_span_image theorem

{m : M} {s : Set ι} : m ∈ span R (b '' s) ↔ ↑(b.repr m).support ⊆ s

Full source

theorem mem_span_image {m : M} {s : Set ι} : m ∈ span R (b '' s)m ∈ span R (b '' s) ↔ ↑(b.repr m).support ⊆ s :=
  ⟨repr_support_subset_of_mem_span _ _, fun h ↦
    span_mono (image_subset _ h) (mem_span_repr_support b _)⟩

Span Membership Criterion via Basis Coordinates

Informal description

Let $M$ be a module over a ring $R$ with basis $b$ indexed by a set $\iota$. For any vector $m \in M$ and any subset $s \subseteq \iota$, the vector $m$ lies in the span of the basis vectors $\{b(i) \mid i \in s\}$ if and only if the support of its coordinate representation $b.\text{repr}(m)$ is contained in $s$. That is: $$ m \in \text{span}_R \{b(i) \mid i \in s\} \leftrightarrow \text{supp}(b.\text{repr}(m)) \subseteq s $$

Basis.self_mem_span_image theorem

[Nontrivial R] {i : ι} {s : Set ι} : b i ∈ span R (b '' s) ↔ i ∈ s

Full source

@[simp]
theorem self_mem_span_image [Nontrivial R] {i : ι} {s : Set ι} :
    b i ∈ span R (b '' s)b i ∈ span R (b '' s) ↔ i ∈ s := by
  simp [mem_span_image, Finsupp.support_single_ne_zero]

Basis Vector in Span of Subset if and only if Index in Subset

Informal description

Let $R$ be a nontrivial ring, $M$ an $R$-module with basis $b$ indexed by $\iota$, and $s \subseteq \iota$. For any $i \in \iota$, the basis vector $b(i)$ lies in the span of $\{b(j) \mid j \in s\}$ if and only if $i \in s$.

Basis.mem_span theorem

(x : M) : x ∈ span R (range b)

Full source

protected theorem mem_span (x : M) : x ∈ span R (range b) :=
  span_mono (image_subset_range _ _) (mem_span_repr_support b x)

Every Vector Lies in the Span of a Basis

Informal description

For any vector $x$ in a module $M$ over a ring $R$ with basis $b$ indexed by $\iota$, the vector $x$ lies in the span of the basis vectors $\{b(i) \mid i \in \iota\}$.

Basis.span_eq theorem

: span R (range b) = ⊤

Full source

@[simp]
protected theorem span_eq : span R (range b) = ⊤ :=
  eq_top_iff.mpr fun x _ => b.mem_span x

Basis Vectors Span the Entire Module

Informal description

For a basis $b$ of a module $M$ over a ring $R$, the span of the basis vectors $\{b(i) \mid i \in \iota\}$ is equal to the entire module $M$.

Basis.index_nonempty theorem

(b : Basis ι R M) [Nontrivial M] : Nonempty ι

Full source

theorem index_nonempty (b : Basis ι R M) [Nontrivial M] : Nonempty ι := by
  obtain ⟨x, y, ne⟩ : ∃ x y : M, x ≠ y := Nontrivial.exists_pair_ne
  obtain ⟨i, _⟩ := not_forall.mp (mt b.ext_elem_iff.2 ne)
  exact ⟨i⟩

Nonempty Index Set for Basis of Nontrivial Module

Informal description

Let $M$ be a nontrivial module over a ring $R$ with a basis $b$ indexed by $\iota$. Then the index set $\iota$ is nonempty.

Basis.linearIndependent theorem

: LinearIndependent R b

Full source

protected theorem linearIndependent : LinearIndependent R b :=
  fun x y hxy => by
    rw [← b.repr_linearCombination x, hxy, b.repr_linearCombination y]

Linear Independence of Basis Vectors

Informal description

For any basis $b$ of a module $M$ over a ring $R$, the family of vectors $(b(i))_{i \in \iota}$ is linearly independent over $R$.

Basis.ne_zero theorem

[Nontrivial R] (i) : b i ≠ 0

Full source

protected theorem ne_zero [Nontrivial R] (i) : b i ≠ 0 :=
  b.linearIndependent.ne_zero i

Nonzero Basis Vectors in Nontrivial Ring

Informal description

For any basis $b$ of a module $M$ over a nontrivial ring $R$ and any index $i$, the basis vector $b(i)$ is nonzero.

Basis.mk definition

: Basis ι R M

Full source

/-- A linear independent family of vectors spanning the whole module is a basis. -/
protected noncomputable def mk : Basis ι R M :=
  .ofRepr
    { hli.repr.comp (LinearMap.id.codRestrict _ fun _ => hsp Submodule.mem_top) with
      invFun := Finsupp.linearCombination _ v
      left_inv := fun x => hli.linearCombination_repr ⟨x, _⟩
      right_inv := fun _ => hli.repr_eq rfl }

Construction of a basis from a spanning linearly independent family

Informal description

Given a linearly independent family of vectors $v : \iota \to M$ over a ring $R$ whose span is the entire module $M$, the function `Basis.mk` constructs a basis for $M$ indexed by $\iota$. This basis provides a linear equivalence between $M$ and the space of finitely supported functions from $\iota$ to $R$, where the basis vectors are exactly the vectors in the family $v$.

Basis.mk_repr theorem

: (Basis.mk hli hsp).repr x = hli.repr ⟨x, hsp Submodule.mem_top⟩

Full source

@[simp]
theorem mk_repr : (Basis.mk hli hsp).repr x = hli.repr ⟨x, hsp Submodule.mem_top⟩ :=
  rfl

Representation of Vectors in Constructed Basis Equals Linear Independence Representation

Informal description

Let $v : \iota \to M$ be a linearly independent family of vectors over a ring $R$ whose span is the entire module $M$, and let $hli$ and $hsp$ be proofs of linear independence and spanning respectively. For any $x \in M$, the representation of $x$ in the basis constructed by `Basis.mk hli hsp` is equal to the representation of $\langle x, hsp \text{Submodule.mem\_top}\rangle$ in the linear independence proof $hli$.

Basis.mk_apply theorem

(i : ι) : Basis.mk hli hsp i = v i

Full source

theorem mk_apply (i : ι) : Basis.mk hli hsp i = v i :=
  show Finsupp.linearCombination _ v _ = v i by simp

Basis Construction Preserves Vectors: $(\text{Basis.mk}\ hli\ hsp)_i = v_i$

Informal description

For any index $i \in \iota$, the $i$-th basis vector constructed via `Basis.mk` from a linearly independent family $v : \iota \to M$ with spanning property equals $v(i)$, i.e., $(\text{Basis.mk}\ hli\ hsp)_i = v_i$.

Basis.coe_mk theorem

: ⇑(Basis.mk hli hsp) = v

Full source

@[simp]
theorem coe_mk : ⇑(Basis.mk hli hsp) = v :=
  funext (mk_apply _ _)

Basis Construction Preserves Vectors: $\text{Basis.mk}\ hli\ hsp = v$

Informal description

Let $v : \iota \to M$ be a linearly independent family of vectors in a module $M$ over a ring $R$ whose span is the entire module $M$. Then the basis constructed from $v$ via `Basis.mk` has the same underlying function as $v$, i.e., $(\text{Basis.mk}\ hli\ hsp)_i = v_i$ for all $i \in \iota$.

Basis.mk_coord_apply_eq theorem

(i : ι) : (Basis.mk hli hsp).coord i (v i) = 1

Full source

/-- Given a basis, the `i`th element of the dual basis evaluates to 1 on the `i`th element of the
basis. -/
theorem mk_coord_apply_eq (i : ι) : (Basis.mk hli hsp).coord i (v i) = 1 :=
  show hli.repr ⟨v i, Submodule.subset_span (mem_range_self i)⟩ i = 1 by simp [hli.repr_eq_single i]

Dual Basis Evaluation at Basis Vector: $\text{coord}_i(v_i) = 1$

Informal description

For a basis constructed from a linearly independent spanning family $v : \iota \to M$ over a ring $R$, the $i$-th coordinate function evaluated at the $i$-th basis vector $v_i$ equals $1$, i.e., $\text{coord}_i(v_i) = 1$.

Basis.mk_coord_apply_ne theorem

{i j : ι} (h : j ≠ i) : (Basis.mk hli hsp).coord i (v j) = 0

Full source

/-- Given a basis, the `i`th element of the dual basis evaluates to 0 on the `j`th element of the
basis if `j ≠ i`. -/
theorem mk_coord_apply_ne {i j : ι} (h : j ≠ i) : (Basis.mk hli hsp).coord i (v j) = 0 :=
  show hli.repr ⟨v j, Submodule.subset_span (mem_range_self j)⟩ i = 0 by
    simp [hli.repr_eq_single j, h]

Vanishing of Dual Basis Elements at Distinct Basis Vectors

Informal description

Let $v : \iota \to M$ be a linearly independent family of vectors spanning a module $M$ over a ring $R$, and let $b$ be the basis constructed from $v$ via `Basis.mk`. For any distinct indices $i, j \in \iota$, the $i$-th coordinate function of $b$ evaluated at $v_j$ is zero, i.e., $b_i(v_j) = 0$.

Basis.mk_coord_apply theorem

[DecidableEq ι] {i j : ι} : (Basis.mk hli hsp).coord i (v j) = if j = i then 1 else 0

Full source

/-- Given a basis, the `i`th element of the dual basis evaluates to the Kronecker delta on the
`j`th element of the basis. -/
theorem mk_coord_apply [DecidableEq ι] {i j : ι} :
    (Basis.mk hli hsp).coord i (v j) = if j = i then 1 else 0 := by
  rcases eq_or_ne j i with h | h
  · simp only [h, if_true, eq_self_iff_true, mk_coord_apply_eq i]
  · simp only [h, if_false, mk_coord_apply_ne h]

Kronecker Delta Property of Dual Basis Vectors

Informal description

Let $v : \iota \to M$ be a linearly independent family of vectors spanning a module $M$ over a ring $R$, and let $b$ be the basis constructed from $v$ via `Basis.mk`. For any indices $i, j \in \iota$, the $i$-th coordinate function of $b$ evaluated at $v_j$ satisfies the Kronecker delta condition: \[ b_i(v_j) = \begin{cases} 1 & \text{if } j = i, \\ 0 & \text{otherwise.} \end{cases} \]

Basis.span definition

: Basis ι R (span R (range v))

Full source

/-- A linear independent family of vectors is a basis for their span. -/
protected noncomputable def span : Basis ι R (span R (range v)) :=
  Basis.mk (linearIndependent_span hli) <| by
    intro x _
    have : ∀ i, v i ∈ span R (range v) := fun i ↦ subset_span (Set.mem_range_self _)
    have h₁ : (((↑) : span R (range v) → M) '' range fun i => ⟨v i, this i⟩) = range v := by
      simp only [SetLike.coe_sort_coe, ← Set.range_comp]
      rfl
    have h₂ : map (Submodule.subtype (span R (range v))) (span R (range fun i => ⟨v i, this i⟩)) =
        span R (range v) := by
      rw [← span_image, Submodule.coe_subtype, h₁]
    have h₃ : (x : M) ∈ map (Submodule.subtype (span R (range v)))
        (span R (Set.range fun i => Subtype.mk (v i) (this i))) := by
      rw [h₂]
      apply Subtype.mem x
    rcases mem_map.1 h₃ with ⟨y, hy₁, hy₂⟩
    have h_x_eq_y : x = y := by
      rw [Subtype.ext_iff, ← hy₂]
      simp
    rwa [h_x_eq_y]

Basis for the span of a linearly independent family

Informal description

Given a linearly independent family of vectors $v : \iota \to M$ over a ring $R$, the structure `Basis.span` constructs a basis for the subspace $\text{span}_R (\text{range } v)$ of $M$ indexed by $\iota$. This basis provides a linear equivalence between the span of $v$ and the space of finitely supported functions from $\iota$ to $R$, where the basis vectors are exactly the vectors in the family $v$.

Basis.span_apply theorem

(i : ι) : (Basis.span hli i : M) = v i

Full source

protected theorem span_apply (i : ι) : (Basis.span hli i : M) = v i :=
  congr_arg ((↑) : span R (range v) → M) <| Basis.mk_apply _ _ _

Basis Vector Equality in Span Construction: $(\text{Basis.span}\ hli)_i = v_i$

Informal description

For any index $i \in \iota$, the $i$-th basis vector of the basis constructed for the span of a linearly independent family $v : \iota \to M$ over a ring $R$ equals $v(i)$, i.e., $(\text{Basis.span}\ hli)_i = v_i$.

Basis.maximal theorem

[Nontrivial R] (b : Basis ι R M) : b.linearIndependent.Maximal

Full source

/-- Any basis is a maximal linear independent set.
-/
theorem maximal [Nontrivial R] (b : Basis ι R M) : b.linearIndependent.Maximal := fun w hi h => by
  -- If `w` is strictly bigger than `range b`,
  apply le_antisymm h
  -- then choose some `x ∈ w \ range b`,
  intro x p
  by_contra q
  -- and write it in terms of the basis.
  have e := b.linearCombination_repr x
  -- This then expresses `x` as a linear combination
  -- of elements of `w` which are in the range of `b`,
  let u : ι ↪ w :=
    ⟨fun i => ⟨b i, h ⟨i, rfl⟩⟩, fun i i' r =>
      b.injective (by simpa only [Subtype.mk_eq_mk] using r)⟩
  simp_rw [Finsupp.linearCombination_apply] at e
  change ((b.repr x).sum fun (i : ι) (a : R) ↦ a • (u i : M)) = ((⟨x, p⟩ : w) : M) at e
  rw [← Finsupp.sum_embDomain (f := u) (g := fun x r ↦ r • (x : M)),
      ← Finsupp.linearCombination_apply] at e
  -- Now we can contradict the linear independence of `hi`
  refine hi.linearCombination_ne_of_not_mem_support _ ?_ e
  simp only [Finset.mem_map, Finsupp.support_embDomain]
  rintro ⟨j, -, W⟩
  simp only [u, Embedding.coeFn_mk, Subtype.mk_eq_mk] at W
  apply q ⟨j, W⟩

Maximality of Linear Independence for Basis Vectors

Informal description

For any nontrivial ring $R$ and any basis $b$ of a module $M$ over $R$, the family of vectors $(b(i))_{i \in \iota}$ is a maximal linearly independent set in $M$. That is, there is no strictly larger family of vectors in $M$ that is linearly independent over $R$.

Basis.uniqueBasis instance

[Subsingleton R] : Unique (Basis ι R M)

Full source

instance uniqueBasis [Subsingleton R] : Unique (Basis ι R M) :=
  ⟨⟨⟨default⟩⟩, fun ⟨b⟩ => by rw [Subsingleton.elim b]⟩

Uniqueness of Basis in Subsingleton Rings

Informal description

For any ring $R$ with a unique element (i.e., $R$ is a subsingleton) and any module $M$ over $R$, there is a unique basis of $M$ indexed by any type $\iota$.

Basis.singleton definition

(ι R : Type*) [Unique ι] [Semiring R] : Basis ι R R

Full source

/-- `Basis.singleton ι R` is the basis sending the unique element of `ι` to `1 : R`. -/
protected def singleton (ι R : Type*) [Unique ι] [Semiring R] : Basis ι R R :=
  ofRepr
    { toFun := fun x => Finsupp.single default x
      invFun := fun f => f default
      left_inv := fun x => by simp
      right_inv := fun f => Finsupp.unique_ext (by simp)
      map_add' := fun x y => by simp
      map_smul' := fun c x => by simp }

Singleton basis

Informal description

Given a type $\iota$ with a unique element and a semiring $R$, the basis `Basis.singleton ι R` is the basis that maps the unique element of $\iota$ to the multiplicative identity $1 \in R$. More precisely, it is constructed as the basis whose representation isomorphism sends any element $x \in R$ to the finitely supported function that takes the value $x$ at the unique element of $\iota$ and zero elsewhere, and whose inverse operation evaluates a finitely supported function at the unique element of $\iota$.

Basis.singleton_apply theorem

(ι R : Type*) [Unique ι] [Semiring R] (i) : Basis.singleton ι R i = 1

Full source

@[simp]
theorem singleton_apply (ι R : Type*) [Unique ι] [Semiring R] (i) : Basis.singleton ι R i = 1 :=
  apply_eq_iff.mpr (by simp [Basis.singleton])

Singleton Basis Vector Equals One

Informal description

For any type $\iota$ with a unique element and any semiring $R$, the basis vector at index $i$ in the singleton basis `Basis.singleton ι R` is equal to the multiplicative identity $1 \in R$.

Basis.singleton_repr theorem

(ι R : Type*) [Unique ι] [Semiring R] (x i) : (Basis.singleton ι R).repr x i = x

Full source

@[simp]
theorem singleton_repr (ι R : Type*) [Unique ι] [Semiring R] (x i) :
    (Basis.singleton ι R).repr x i = x := by simp [Basis.singleton, Unique.eq_default i]

Representation of Singleton Basis Evaluates to Input Value

Informal description

Let $\iota$ be a type with a unique element, $R$ a semiring, and $x \in R$. For the singleton basis `Basis.singleton ι R`, the representation of $x$ evaluated at any index $i \in \iota$ equals $x$, i.e., $\text{repr}(\text{Basis.singleton } \iota R)(x)(i) = x$.

Basis.empty definition

[Subsingleton M] [IsEmpty ι] : Basis ι R M

Full source

/-- If `M` is a subsingleton and `ι` is empty, this is the unique `ι`-indexed basis for `M`. -/
protected def empty [Subsingleton M] [IsEmpty ι] : Basis ι R M :=
  ofRepr 0

Empty basis for a subsingleton module

Informal description

Given a module $M$ that is a subsingleton (i.e., has at most one element) and an empty index type $\iota$, this is the unique $\iota$-indexed basis for $M$. The basis is constructed using the zero linear equivalence, since $M$ is trivial when it is a subsingleton.

Basis.emptyUnique instance

[Subsingleton M] [IsEmpty ι] : Unique (Basis ι R M)

Full source

instance emptyUnique [Subsingleton M] [IsEmpty ι] : Unique (Basis ι R M) where
  default := Basis.empty M
  uniq := fun _ => congr_arg ofRepr <| Subsingleton.elim _ _

Uniqueness of the Empty Basis for a Subsingleton Module

Informal description

For any subsingleton module $M$ over a ring $R$ and an empty index type $\iota$, there is a unique basis of $M$ indexed by $\iota$.

Basis.noZeroSMulDivisors theorem

[NoZeroDivisors R] (b : Basis ι R M) : NoZeroSMulDivisors R M

Full source

protected theorem noZeroSMulDivisors [NoZeroDivisors R] (b : Basis ι R M) :
    NoZeroSMulDivisors R M :=
  ⟨fun {c x} hcx => by
    exact or_iff_not_imp_right.mpr fun hx => by
      rw [← b.linearCombination_repr x, ← LinearMap.map_smul,
        ← map_zero (linearCombination R b)] at hcx
      have := b.linearIndependent hcx
      rw [smul_eq_zero] at this
      exact this.resolve_right fun hr => hx (b.repr.map_eq_zero_iff.mp hr)⟩

Basis Implies No Zero Scalar Divisors in Modules over Rings without Zero Divisors

Informal description

Let $R$ be a ring with no zero divisors, and let $M$ be a module over $R$ with a basis $b$ indexed by $\iota$. Then $M$ has no zero scalar divisors, i.e., for any $c \in R$ and $x \in M$, $c \cdot x = 0$ implies $c = 0$ or $x = 0$.

Basis.smul_eq_zero theorem

[NoZeroDivisors R] (b : Basis ι R M) {c : R} {x : M} : c • x = 0 ↔ c = 0 ∨ x = 0

Full source

protected theorem smul_eq_zero [NoZeroDivisors R] (b : Basis ι R M) {c : R} {x : M} :
    c • x = 0 ↔ c = 0 ∨ x = 0 :=
  @smul_eq_zero _ _ _ _ _ b.noZeroSMulDivisors _ _

Scalar Multiplication Zero Criterion for Modules with Basis over No-Zero-Divisor Rings

Informal description

Let $R$ be a ring with no zero divisors, and let $M$ be a module over $R$ with a basis $b$ indexed by $\iota$. For any scalar $c \in R$ and any vector $x \in M$, the scalar multiplication $c \cdot x$ equals zero if and only if $c = 0$ or $x = 0$.

Basis.basis_singleton_iff theorem

 {R M : Type*} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (ι : Type*) [Unique ι] :
  Nonempty (Basis ι R M) ↔ ∃ x ≠ 0, ∀ y : M, ∃ r : R, r • x = y

Full source

theorem basis_singleton_iff {R M : Type*} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M]
    [NoZeroSMulDivisors R M] (ι : Type*) [Unique ι] :
    NonemptyNonempty (Basis ι R M) ↔ ∃ x ≠ 0, ∀ y : M, ∃ r : R, r • x = y := by
  constructor
  · rintro ⟨b⟩
    refine ⟨b default, b.linearIndependent.ne_zero _, ?_⟩
    simpa [span_singleton_eq_top_iff, Set.range_unique] using b.span_eq
  · rintro ⟨x, nz, w⟩
    refine ⟨ofRepr <| LinearEquiv.symm
      { toFun := fun f => f default • x
        invFun := fun y => Finsupp.single default (w y).choose
        left_inv := fun f => Finsupp.unique_ext ?_
        right_inv := fun y => ?_
        map_add' := fun y z => ?_
        map_smul' := fun c y => ?_ }⟩
    · simp [Finsupp.add_apply, add_smul]
    · simp only [Finsupp.coe_smul, Pi.smul_apply, RingHom.id_apply]
      rw [← smul_assoc]
    · refine smul_left_injective _ nz ?_
      simp only [Finsupp.single_eq_same]
      exact (w (f default • x)).choose_spec
    · simp only [Finsupp.single_eq_same]
      exact (w y).choose_spec

Existence of Singleton Basis in Modules over Nontrivial Rings

Informal description

Let $R$ be a nontrivial ring, $M$ a module over $R$ with no zero scalar divisors, and $\iota$ a type with a unique element. Then there exists a basis for $M$ indexed by $\iota$ if and only if there exists a nonzero element $x \in M$ such that every $y \in M$ can be written as $y = r \cdot x$ for some $r \in R$.

Main results