Submodule.mem_top
theorem Submodule.mem_top :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M},
x ∈ ⊤
This theorem states that for any semiring `R` and additive commutative monoid `M` that forms a module over `R`, every element `x` of `M` belongs to the top element `⊤` of the submodule lattice. In other words, all elements of a module are included in the universal submodule.
More concisely: For any semiring `R` and additive commutative monoid `M` being an `R`-module, every element of `M` belongs to the top element of the submodule lattice.
|
Submodule.ne_bot_iff
theorem Submodule.ne_bot_iff :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(p : Submodule R M), p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ 0
This theorem states that for all types `R` and `M`, where `R` is a semiring, `M` is an additive commutative monoid, and `M` is a module over `R`, a submodule `p` of `M` is not the bottom element if and only if there exists an element `x` in `p` such that `x` is not the zero element. In mathematical terms, $\forall R, M, p$, where $R$ is a semiring, $M$ is a module over $R$, and $p$ is a submodule of $M$, $p \neq \bot$ if and only if $\exists x \in p$, $x \neq 0$.
More concisely: A submodule of an R-module M, where R is a semiring, is non-empty if and only if it contains a non-zero element.
|
Submodule.disjoint_def
theorem Submodule.disjoint_def :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{p p' : Submodule R M}, Disjoint p p' ↔ ∀ x ∈ p, x ∈ p' → x = 0
The theorem `Submodule.disjoint_def` defines what it means for two submodules `p` and `p'` of a module `M` over a semiring `R` to be disjoint. Specifically, it states that two submodules are disjoint if and only if for all elements `x` from the given module, if `x` is in both `p` and `p'`, then `x` must be the zero vector. This corresponds to the general concept of disjointness in lattice theory, where two elements are disjoint if their infimum is the bottom element. In the context of submodules, the 'bottom element' is the zero vector.
More concisely: Two submodules of a module over a semiring are disjoint if and only if their intersection is the submodule generated by the zero vector.
|
Submodule.top_coe
theorem Submodule.top_coe :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
↑⊤ = Set.univ
The theorem `Submodule.top_coe` states that for any type `R` representing a semiring, a type `M` representing an additive commutative monoid, and given that `M` is an `R`-module, the top submodule (denoted as `⊤`) when coerced to a set, is equal to the universal set (`Set.univ`). In mathematical terms, this means that all elements of the module type `M` are included in the top submodule, making it equivalent to the universal set of `M`.
More concisely: For any semiring `R` and an additive commutative monoid `M` being an `R`-module, the top submodule of `M` equals the universal set of `M`.
|
Submodule.mem_iInf
theorem Submodule.mem_iInf :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_4}
(p : ι → Submodule R M) {x : M}, x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i
The theorem `Submodule.mem_iInf` states that for any types `R` and `M`, given a semiring structure on `R`, an additive commutative monoid structure on `M`, and a module structure over `R` on `M`, and for any indexing type `ι`, a function `p` from `ι` to submodules of `M`, and an element `x` of `M`, `x` belongs to the intersection of all submodules `p i` (for all `i` in `ι`) if and only if `x` belongs to each individual submodule `p i`.
More concisely: For any semiring `R`, additive commutative monoid `M`, module `M` over `R`, indexing type `ι`, and submodule functions `p : ι → submodules M`, an element `x` of `M` belongs to the intersection of all `p i` if and only if it belongs to each `p i`.
|
Submodule.eq_bot_iff
theorem Submodule.eq_bot_iff :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(p : Submodule R M), p = ⊥ ↔ ∀ x ∈ p, x = 0
This theorem states that for any given set of objects `p` considered as a submodule of a `Module` M over a `Semiring` R, `p` is equal to the zero submodule (denoted by `⊥`) if and only if every element `x` within `p` is equal to zero. Here, `Module` and `Semiring` are algebraic structures in mathematics. `Module` is a generalization of vector spaces and `Semiring` is a set with two binary operations that generalize the arithmetic operations of addition and multiplication.
More concisely: A submodule `p` of a Module M over a Semiring R is the zero submodule if and only if every element in `p` is the additive identity (zero).
|
Submodule.iInf_coe
theorem Submodule.iInf_coe :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_4}
(p : ι → Submodule R M), ↑(⨅ i, p i) = ⋂ i, ↑(p i)
This theorem, `Submodule.iInf_coe`, states that for any indexed collection of submodules `p` of a module `M` over a semiring `R`, the set theoretic intersection of the underlying sets of all these submodules (`⋂ i, ↑(p i)`) is the same as the underlying set of the infimum of all these submodules (`↑(⨅ i, p i)`). In other words, taking the intersection of the submodules in the set context is equivalent to taking the infimum in the submodule context.
More concisely: For any indexed collection of submodules `p` of a module `M` over a semiring `R`, the set-theoretic intersection of their underlying sets equals the underlying set of the infimum of these submodules.
|
Mathlib.Algebra.Module.Submodule.Lattice._auxLemma.2
theorem Mathlib.Algebra.Module.Submodule.Lattice._auxLemma.2 :
∀ {S : Type u_4} {M : Type u_5} [inst : Zero M] [inst_1 : SetLike S M] [self : ZeroMemClass S M] (s : S),
(0 ∈ s) = True
This theorem, `Mathlib.Algebra.Module.Submodule.Lattice._auxLemma.2`, states that for any SetLike structure `S` (a structure that behaves like a set) over a type `M` which has a zero element, and any element `s` of type `S` within the context where `S` is a `ZeroMemClass` (a class with a property that zero is in the set), the statement that "zero is an element of `s`" is always true.
More concisely: For any SetLike structure over a type with a zero element, zero is an element of every such structure where zero is a member.
|
Submodule.mem_sup_left
theorem Submodule.mem_sup_left :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{S T : Submodule R M} {x : M}, x ∈ S → x ∈ S ⊔ T
This theorem states that for any semiring `R`, any `AddCommMonoid` `M`, and any `Module` `R M`, if `x` is an element of the submodule `S`, then `x` is also an element of the sup (supremum or least upper bound) of the submodules `S` and `T`. This implies that any element in a particular submodule is also found within the sup of that submodule and another.
More concisely: For any semiring `R`, `AddCommMonoid` `M`, and `Module` `R M`, if `x` is an element of `S` and `S`, `T` are submodules of `M`, then `x` lies in the supremum of `S` and `T`.
|
Submodule.eq_top_iff'
theorem Submodule.eq_top_iff' :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{p : Submodule R M}, p = ⊤ ↔ ∀ (x : M), x ∈ p
This theorem states that for any type `R` with a semiring structure, any type `M` with an additive commutative monoid structure, and `M` being a module over `R`, a submodule `p` of `M` is equal to the top submodule if and only if all elements of `M` are contained in `p`. In other words, a submodule is the entire module itself if it contains every element of the module.
More concisely: A submodule of an `R`-module `M` is equal to the entire module if and only if every element of `M` is contained in the submodule.
|
Submodule.mem_sInf
theorem Submodule.mem_sInf :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{S : Set (Submodule R M)} {x : M}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
This theorem states that, for any semiring `R`, any additive commutative monoid `M`, and any `R`-module `M`, for any set `S` of submodules of `M`, and any element `x` of `M`, `x` is an element of the infimum of `S` if and only if `x` is an element of every submodule `p` in `S`. Here, the infimum of a set of submodules is the largest submodule that is contained in all submodules in the set.
More concisely: For any semiring `R`, additive commutative monoid `M`, and `R`-module `M`, an element `x` of `M` belongs to the infimum of a set `S` of submodules of `M` if and only if `x` is contained in every submodule `p` in `S`.
|
Mathlib.Algebra.Module.Submodule.Lattice._auxLemma.11
theorem Mathlib.Algebra.Module.Submodule.Lattice._auxLemma.11 :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_4}
(p : ι → Submodule R M) {x : M}, (x ∈ ⨅ i, p i) = ∀ (i : ι), x ∈ p i
This theorem states that for any semiring `R`, any additive commutative monoid `M` and a module structure over `M` and `R`, any indexing type `ι`, and any family of submodules `p` indexed by `ι`, an element `x` of `M` belongs to the intersection of all submodules (⨅ i, p i) if and only if `x` belongs to each submodule `p i` for every `i` in `ι`. This is a characterization of membership in the intersection of a family of submodules in terms of membership in each individual submodule.
More concisely: For any semiring R, additive commutative monoid M with an R-module structure, indexing type ι, and family of submodules p indexed by ι, an element x of M belongs to the intersection of all p i if and only if x is in each p i for all i in ι.
|
Mathlib.Algebra.Module.Submodule.Lattice._auxLemma.5
theorem Mathlib.Algebra.Module.Submodule.Lattice._auxLemma.5 :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M},
(x ∈ ⊤) = True
This theorem states that, for any semiring `R`, any additive commutative monoid `M`, and any module `R M` over the semiring and the monoid, any element `x` of `M` is an element of the top element of the lattice structure (denoted by `⊤`). In other words, all elements of the module belong to the top of the lattice structure, a statement that is always true.
More concisely: For any semiring `R`, additive commutative monoid `M`, and `R`-module `M`, every element of `M` is contained in the top element of the lattice of `R`-submodules of `M`.
|
Submodule.mem_sup_right
theorem Submodule.mem_sup_right :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{S T : Submodule R M} {x : M}, x ∈ T → x ∈ S ⊔ T
This theorem, `Submodule.mem_sup_right`, states that for any semiring `R`, additively commutative monoid `M`, and module `M` over `R`, and for any two submodules `S` and `T` of `M`, if a member `x` belongs to submodule `T`, then `x` also belongs to the supremum of `S` and `T`, denoted as `S ⊔ T`. In the context of module theory, the supremum of two submodules is the smallest submodule that includes both submodules.
More concisely: For any semiring `R`, additively commutative monoid `M`, and module `M` over `R`, if `x` is an element of submodule `T` of `M`, then `x` belongs to the supremum `S ⊔ T` of submodules `S` and `T` of `M`.
|
Submodule.mem_bot
theorem Submodule.mem_bot :
∀ (R : Type u_1) {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M},
x ∈ ⊥ ↔ x = 0
This theorem states that for any semiring `R` and any additive commutative monoid `M` that is a module over `R`, any element `x` of `M` is in the bottom submodule (denoted by `⊥`) if and only if `x` is equal to zero. In other words, the bottom submodule only contains the zero element.
More concisely: For any semiring `R` and additive commutative `R`-module `M`, the bottom submodule `⊥` equals the additive subgroup generated by the zero element.
|
Submodule.mem_iSup_of_mem
theorem Submodule.mem_iSup_of_mem :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_4}
{b : M} {p : ι → Submodule R M} (i : ι), b ∈ p i → b ∈ ⨆ i, p i
This theorem states that for any semiring `R`, an additively commutative monoid `M`, and a module `M` over `R`, given an index type `ι` and a function `p` from `ι` to submodules of `M`, if an element `b` of `M` is in the image of `p` at index `i`, then `b` belongs to the supremum of the images of `p` over all indices. In simpler terms, if an element is in a particular submodule, it is also in the supremum of all the submodules.
More concisely: For any semiring `R`, additively commutative monoid `M`, and `R`-module `M`, if `p` is a function from an index type `ι` to submodules of `M` such that `b ∈ p i` for some index `i`, then `b ∈ ⨆ (j : ι) p j`.
|
Submodule.mem_inf
theorem Submodule.mem_inf :
∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{p q : Submodule R M} {x : M}, x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q
This theorem states that for any semiring `R`, additive commutative monoid `M`, and `R`-module `M`, given two submodules `p` and `q` of `M` and an element `x` of `M`, `x` is in the intersection of `p` and `q` if and only if `x` is in `p` and `x` is in `q`. In other words, the intersection of two submodules is defined as the set of elements that belong to both submodules.
More concisely: For any semiring `R`, additive commutative monoid `M`, and `R`-module `M`, the intersection of submodules `p` and `q` of `M` is equal to the set of elements `x` in `M` such that `x` belongs to both `p` and `q` (i.e., `x` is in `p` and `x` is in `q`).
|
Mathlib.Algebra.Module.Submodule.Lattice._auxLemma.1
theorem Mathlib.Algebra.Module.Submodule.Lattice._auxLemma.1 :
∀ (R : Type u_1) {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M},
(x ∈ ⊥) = (x = 0)
This theorem states that for any semiring `R` and for any module `M` over `R`, an element `x` belongs to the zero submodule (denoted as `⊥`) if and only if `x` is equal to the zero element. Here, `Semiring R` implies that `R` is a semiring, `AddCommMonoid M` implies that `M` is an additive commutative monoid, and `Module R M` implies that `M` is a module over the semiring `R`. The zero submodule `⊥` of `M` is the set containing only the zero element of `M`.
More concisely: For any semiring `R` and module `M` over `R`, an element `x` in `M` is in the zero submodule if and only if `x` is the zero element of `M`.
|