Mathlib.Algebra.Module.Submodule.Basic._auxLemma.1
theorem Mathlib.Algebra.Module.Submodule.Basic._auxLemma.1 :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
(x : M), (x ∈ p.toAddSubmonoid) = (x ∈ p)
This theorem, `Mathlib.Algebra.Module.Submodule.Basic._auxLemma.1`, states that for all semirings `R`, additive commutative monoids `M`, and `R`-modules `M`, for any submodule `p` of `M` and any element `x` of `M`, `x` belongs to the additive submonoid of `p` if and only if `x` belongs to `p`. In other words, the membership of an element in the submodule's underlying additive submonoid is the same as the membership in the submodule itself.
More concisely: For any semiring R, additive commutative monoid M, and R-module M, an element x of M belongs to the additive submonoid of a submodule p if and only if x is in p.
|
Submodule.zero_mem
theorem Submodule.zero_mem :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
(p : Submodule R M), 0 ∈ p
This theorem, `Submodule.zero_mem`, states that for any given submodule `p` of a module `M` over a semiring `R`, the zero element of the module is always an element of the submodule. Here, `R` is a semiring, `M` is an additive commutative monoid such that `M` is a module over `R`, and `p` is a submodule of `M`.
More concisely: For any submodule `p` of an additive commutative monoid `M` over a semiring `R`, the additive identity of `M` belongs to `p`.
|
Submodule.sum_mem
theorem Submodule.sum_mem :
∀ {R : Type u} {M : Type v} {ι : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
(p : Submodule R M) {t : Finset ι} {f : ι → M}, (∀ c ∈ t, f c ∈ p) → (t.sum fun i => f i) ∈ p
The theorem `Submodule.sum_mem` states that for any semiring `R`, any additive commutative monoid `M`, and any type `ι`, given a module structure on `M` over `R`, a submodule `p` of `M`, a finite set `t` of elements of type `ι`, and a function `f` mapping elements of `ι` to `M`, if every element `c` in `t` maps to an element in `p` under `f`, then the sum of `f(i)` for all `i` in `t` is also an element of `p`. In simpler terms, the sum of elements in a submodule, obtained via a function on a finite set, remains in the submodule.
More concisely: If `M` is an additive commutative monoid with an `R`-module structure, `p` is a submodule of `M`, `t` is a finite set, and for all `i` in `t`, `f(i)` is in `p`, then `∑ i in t, f(i)` is in `p`.
|
Submodule.smul_mem
theorem Submodule.smul_mem :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
(p : Submodule R M) {x : M} (r : R), x ∈ p → r • x ∈ p
This theorem, `Submodule.smul_mem`, states that for any semiring `R`, additively commutative monoid `M`, and `Module R M` as well as any element `x` of `M` and scalar `r` from `R`, if `x` is an element of a submodule `p` of `M`, then the scalar multiple `r • x` is also an element of the submodule `p`. In other words, the submodule `p` is closed under scalar multiplication from `R`.
More concisely: If `p` is a submodule of an additively commutative monoid `M` over a semiring `R`, then for all `x in p` and `r in R`, `r • x` is also in `p`.
|
Submodule.toAddSubmonoid_injective
theorem Submodule.toAddSubmonoid_injective :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Function.Injective Submodule.toAddSubmonoid
The theorem `Submodule.toAddSubmonoid_injective` asserts that for any given semiring `R`, an additive commutative monoid `M`, and any given module of `R` and `M`, the function `Submodule.toAddSubmonoid`, which reinterprets a `Submodule` as an `AddSubmonoid`, is injective. This means that if this function maps two different `Submodule`s to the same `AddSubmonoid`, those `Submodule`s were actually the same to begin with, hence ensuring the uniqueness of `Submodule`s in this context.
More concisely: The function `Submodule.toAddSubmonoid` mapping submodules of an abelian semigroup to its additive submonoids is an injection.
|
Mathlib.Algebra.Module.Submodule.Basic._auxLemma.6
theorem Mathlib.Algebra.Module.Submodule.Basic._auxLemma.6 :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
(p : Submodule R M), (0 ∈ p) = True
This theorem states that for any semiring `R`, any additive commutative monoid `M`, and any `R`-module structure on `M`, zero is an element of any submodule `p` of `M`. In other words, the submodule of a module over a semiring always contains the zero element.
More concisely: For any semiring `R`, any additive commutative monoid `M` with an `R`-module structure, every submodule `p` of `M` contains the additive identity `0` of `M`.
|
Submodule.mk_eq_zero
theorem Submodule.mk_eq_zero :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
(p : Submodule R M) {x : M} (h : x ∈ p), ⟨x, h⟩ = 0 ↔ x = 0
This theorem states that for any semiring `R`, commutative add monoid `M`, and `M` as an `R`-module, given a submodule `p` of `M` and an element `x` of `M` such that `x` belongs to the submodule `p`, the submodule element denoted by `{ val := x, property := h }` is equal to the zero element if and only if `x` itself is the zero element. Essentially, it asserts that an element of a submodule is zero if and only if the corresponding element in the original module is zero.
More concisely: For any semiring R, commutative add monoid M, and R-module structure on M, an element x of M belongs to the submodule p if and only if the submodule element {val := x, property := h} equals the zero element. In other words, x is in the submodule p if and only if the submodule element representing x is zero.
|
Submodule.neg_mem
theorem Submodule.neg_mem :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
{x : M}, x ∈ p → -x ∈ p
This theorem states that for any ring 'R' and additive commutative group 'M' with 'M' being a module over 'R', and for any submodule 'p' of 'M', if an element 'x' belongs to 'p', then the additive inverse of 'x' (represented as '-x') also belongs to 'p'. In other words, if a submodule includes a certain element, it also includes the negation of that element.
More concisely: If 'p' is a submodule of the additive commutative group 'M' over the ring 'R', then for all 'x' in 'p', we have '-x' (the additive inverse of 'x') also in 'p'.
|
Submodule.smul_of_tower_mem
theorem Submodule.smul_of_tower_mem :
∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
(p : Submodule R M) {x : M} [inst_2 : SMul S R] [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (r : S),
x ∈ p → r • x ∈ p
This theorem states that for any types `S`, `R`, and `M`, where `R` is a semiring, `M` is an additive commutative monoid, and `M` is a `R`-Module, given a submodule `p` of `M` over `R`, any element `x` of `M`, and operations of scalar multiplication of `S` on `R` and `M`, if `S`, `R`, and `M` form a scalar tower, then for any scalar `r` from `S`, if `x` is an element of the submodule `p`, then `r` scaled by `x`, denoted as `r • x`, is also an element of the submodule `p`.
In other words, it states that a submodule of a module is closed under scalar multiplication, in the context of a scalar tower. A scalar tower is a situation where scalar multiplication is compatible in a layered manner, i.e., for three types `S`, `R`, and `M`, if `S` and `R` are semirings, `M` is an `R`-module, and there is scalar multiplication of `S` on `R` and `M`, the multiplication `s • (r • m)` is the same as `(s • r) • m` for any `s` in `S`, `r` in `R`, and `m` in `M`.
More concisely: In a scalar tower of types `S`, `R`, and `M` where `M` is an additive commutative `R`-module, any submodule `p` of `M` is closed under scalar multiplication by elements of `S`.
|
Submodule.sub_mem
theorem Submodule.sub_mem :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
{x y : M}, x ∈ p → y ∈ p → x - y ∈ p
This theorem, `Submodule.sub_mem`, states that for any ring `R` and any additive commutative group `M` which is a module over `R`, and any submodule `p` of `M`, if `x` and `y` are both elements of `p`, then the subtraction of `y` from `x` is also an element of `p`. This theorem essentially asserts the closed property of subtraction operation in the context of a submodule.
More concisely: For any ring `R`, additive commutative group `M` being an `R`-module, and submodule `p` of `M`, if `x, y ∈ p`, then `x - y ∈ p`.
|
Submodule.add_mem
theorem Submodule.add_mem :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
(p : Submodule R M) {x y : M}, x ∈ p → y ∈ p → x + y ∈ p
This theorem, `Submodule.add_mem`, states that for any semiring `R` and any additively commutative monoid `M` that is also a module over `R`, and any submodule `p` of `M`, if `x` and `y` are elements of `p`, then their sum `x + y` is also in `p`. Essentially, this theorem guarantees that the sum of any two elements in a submodule remains within that submodule.
More concisely: For any semiring R, additively commutative monoid M being an R-module, and submodule p of M, if x, y ∈ p then x + y ∈ p.
|
Submodule.smul_mem'
theorem Submodule.smul_mem' :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(self : Submodule R M) (c : R) {x : M}, x ∈ self.carrier → c • x ∈ self.carrier
This theorem states that the carrier set of a submodule is closed under scalar multiplication. In other words, given any scalar 'c' from a semiring 'R' and any element 'x' from the carrier set of a submodule in the module 'M' (over 'R'), the scalar product 'c' multiplied by 'x' will also be an element of the carrier set. Here, 'M' is a module over 'R' which forms a semiring and is also an additive commutative monoid.
More concisely: If 'M' is a submodule of an additive commutative monoid that is also a semiring over a semiring 'R', then for all scalars 'c' in 'R' and elements 'x' in 'M', the scalar product 'cx' is in the submodule.
|
Submodule.mem_toAddSubmonoid
theorem Submodule.mem_toAddSubmonoid :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
(x : M), x ∈ p.toAddSubmonoid ↔ x ∈ p
The theorem `Submodule.mem_toAddSubmonoid` states that for any semiring `R`, any additive commutative monoid `M` that is also a module over `R`, any submodule `p` of `M`, and any element `x` of `M`, `x` is a member of the additive submonoid associated with `p` if and only if `x` is a member of `p` itself. Essentially, it establishes the equivalence of membership between a submodule and its corresponding additive submonoid in the context of module theory.
More concisely: For any semiring R, additive commutative monoid and R-module M, submodule p, and element x of M, x belongs to the additive submonoid of p if and only if x belongs to p.
|
Submodule.ext
theorem Submodule.ext :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{p q : Submodule R M}, (∀ (x : M), x ∈ p ↔ x ∈ q) → p = q
The theorem `Submodule.ext` asserts that for any two submodules `p` and `q` of a module `M` over a semiring `R`, if every element `x` of `M` is in `p` if and only if it is in `q`, then `p` and `q` are the same submodule. In other words, two submodules are equal if they contain exactly the same elements.
More concisely: If two submodules of a module contain the same elements, then they are equal.
|
Mathlib.Algebra.Module.Submodule.Basic._auxLemma.12
theorem Mathlib.Algebra.Module.Submodule.Basic._auxLemma.12 :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
{x : M}, (x ∈ p.toAddSubgroup) = (x ∈ p)
This theorem states that for any type `R` of ring, any type `M` of additive commutative group and any `p` which is a submodule of type `M` over the ring `R`, an element `x` of type `M` belongs to the additive subgroup corresponding to the submodule `p` if and only if `x` belongs to the submodule `p`. In other words, it guarantees that the set of elements contained in a submodule, when viewed as an additive subgroup, remains unchanged.
More concisely: For any ring R, additive commutative group M, and submodule p of M, the submodule p and the additive subgroup generated by p are equal.
|
Submodule.smul_mem_iff
theorem Submodule.smul_mem_iff :
∀ {S : Type u'} {R : Type u} {M : Type v} [inst : DivisionSemiring S] [inst_1 : Semiring R]
[inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : SMul S R] [inst_5 : Module S M]
[inst_6 : IsScalarTower S R M] (p : Submodule R M) {s : S} {x : M}, s ≠ 0 → (s • x ∈ p ↔ x ∈ p)
This theorem states that for a given division semiring `S`, semiring `R`, and an additive commutative monoid `M`, which are structured such that `M` is an `R`-module and an `S`-module, and `S` acts on `R` which further acts on `M` (forming a scalar tower), then for any submodule `p` of the `R`-module `M`, a scalar `s` in `S`, and an element `x` in `M`, if `s` is not zero, then `s` times `x` belongs to the submodule `p` if and only if `x` belongs to `p`. In simpler terms, a nonzero scalar multiple of an element is in a submodule if and only if the original element is in that submodule.
More concisely: For an `R`-module `M` over a division semiring `S`, if `p` is an `R`-submodule and `s` is a nonzero scalar in `S`, then `s * x ∈ p` if and only if `x ∈ p` for any `x` in `M`.
|
Submodule.neg_mem_iff
theorem Submodule.neg_mem_iff :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
{x : M}, -x ∈ p ↔ x ∈ p
This theorem states that for any ring `R`, additive commutative group `M`, and module `M` over `R`, given a submodule `p` of `M` and any element `x` of `M`, the additive inverse of `x` (`-x`) is in the submodule `p` if and only if `x` is in `p`. In other words, a submodule of a module over a ring is closed under taking additive inverses.
More concisely: For any submodule `p` of an additive commutative group `M` over a ring `R`, if `x` is an element of `p`, then `-x` is also an element of `p`, and conversely.
|