SModEq.top
theorem SModEq.top :
∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M},
x ≡ y [SMOD ⊤]
This theorem states that for any ring `R` and its associated module `M`, any two elements `x` and `y` from the module `M` are congruent modulo the top element, denoted by `⊤`. This congruence is true irrespective of the actual values of `x` and `y`. In other words, in the context of a module over a ring, all elements are congruent under the highest (top) modular relation.
More concisely: In any ring R and its module M, all elements x and y in M are congruent modulo the top element ⊤.
|
SModEq.refl
theorem SModEq.refl :
∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
(x : M), x ≡ x [SMOD U]
The theorem `SModEq.refl` states that for any given ring `R`, commutative additive group `M`, `M` being a `R`-module, and `U` being a submodule of `M`, every element `x` of `M` is congruent to itself modulo `U`. In other words, for any `x` in `M`, the statement `x ≡ x [SMOD U]` is always true. This is the reflexivity property in the context of an equivalence relation modulo a submodule.
More concisely: For any `R`-module `M` and submodule `U`, every element `x` in `M` is congruent to `x` modulo `U`.
|