modular equivalence for submodule

def SModEq {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] (U : Submodule R M) (x y : M) : Prop

A predicate saying two elements of a module are equivalent modulo a submodule.

Equations

• (x ≡ y [SMOD U]) = (Submodule.Quotient.mk x = Submodule.Quotient.mk y)

def «term_≡_[SMOD_]» : Lean.TrailingParserDescr

A predicate saying two elements of a module are equivalent modulo a submodule.

Equations

• One or more equations did not get rendered due to their size.

theorem SModEq.def {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} : x ≡ y [SMOD U] ↔ Submodule.Quotient.mk x = Submodule.Quotient.mk y

theorem SModEq.sub_mem {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} : x ≡ y [SMOD U] ↔ x - y ∈ U

@[simp]

theorem SModEq.top {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {x y : M} : x ≡ y [SMOD ⊤]

@[simp]

theorem SModEq.bot {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {x y : M} : x ≡ y [SMOD ⊥] ↔ x = y

theorem SModEq.mono {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U₁ U₂ : Submodule R M} {x y : M} (HU : U₁ ≤ U₂) (hxy : x ≡ y [SMOD U₁]) : x ≡ y [SMOD U₂]

theorem SModEq.of_toAddSubgroup_le {R : Type u_1} [Ring R] {S : Type u_2} [Ring S] {M : Type u_4} [AddCommGroup M] [Module R M] [Module S M] {U : Submodule R M} {V : Submodule S M} (h : U.toAddSubgroup ≤ V.toAddSubgroup) {x y : M} (hxy : x ≡ y [SMOD U]) : x ≡ y [SMOD V]

@[simp]

theorem SModEq.refl {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} (x : M) : x ≡ x [SMOD U]

theorem SModEq.rfl {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} : x ≡ x [SMOD U]

theorem SModEq.symm {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} (hxy : x ≡ y [SMOD U]) : y ≡ x [SMOD U]

theorem SModEq.comm {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} : x ≡ y [SMOD U] ↔ y ≡ x [SMOD U]

theorem SModEq.trans {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y z : M} (hxy : x ≡ y [SMOD U]) (hyz : y ≡ z [SMOD U]) : x ≡ z [SMOD U]

instance SModEq.instIsEquiv {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} : IsEquiv M (SModEq U)

theorem SModEq.add {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x₁ x₂ y₁ y₂ : M} (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ + x₂ ≡ y₁ + y₂ [SMOD U]

theorem SModEq.sum {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {ι : Type u_6} {s : Finset ι} {x y : ι → M} (hxy : ∀ i ∈ s, x i ≡ y i [SMOD U]) : ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]

theorem SModEq.smul {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} (hxy : x ≡ y [SMOD U]) (c : R) : c • x ≡ c • y [SMOD U]

theorem SModEq.nsmul {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} (hxy : x ≡ y [SMOD U]) (n : ℕ) : n • x ≡ n • y [SMOD U]

theorem SModEq.zsmul {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} (hxy : x ≡ y [SMOD U]) (n : ℤ) : n • x ≡ n • y [SMOD U]

theorem SModEq.mul {A : Type u_3} [CommRing A] {I : Ideal A} {x₁ x₂ y₁ y₂ : A} (hxy₁ : x₁ ≡ y₁ [SMOD I]) (hxy₂ : x₂ ≡ y₂ [SMOD I]) : x₁ * x₂ ≡ y₁ * y₂ [SMOD I]

theorem SModEq.prod {A : Type u_3} [CommRing A] {I : Ideal A} {ι : Type u_6} {s : Finset ι} {x y : ι → A} (hxy : ∀ i ∈ s, x i ≡ y i [SMOD I]) : ∏ i ∈ s, x i ≡ ∏ i ∈ s, y i [SMOD I]

theorem SModEq.pow {A : Type u_3} [CommRing A] {I : Ideal A} {x y : A} (n : ℕ) (hxy : x ≡ y [SMOD I]) : x ^ n ≡ y ^ n [SMOD I]

theorem SModEq.neg {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} (hxy : x ≡ y [SMOD U]) : -x ≡ -y [SMOD U]

theorem SModEq.sub {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x₁ x₂ y₁ y₂ : M} (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ - x₂ ≡ y₁ - y₂ [SMOD U]

theorem SModEq.zero {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} : x ≡ 0 [SMOD U] ↔ x ∈ U

theorem sub_smodEq_zero {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} : x - y ≡ 0 [SMOD U] ↔ x ≡ y [SMOD U]

theorem SModEq.map {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} {N : Type u_5} [AddCommGroup N] [Module R N] (hxy : x ≡ y [SMOD U]) (f : M →ₗ[R] N) : f x ≡ f y [SMOD Submodule.map f U]

theorem SModEq.comap {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {x y : M} {N : Type u_5} [AddCommGroup N] [Module R N] (V : Submodule R N) {f : M →ₗ[R] N} (hxy : f x ≡ f y [SMOD V]) : x ≡ y [SMOD Submodule.comap f V]

theorem SModEq.eval {R : Type u_6} [CommRing R] {I : Ideal R} {x y : R} (h : x ≡ y [SMOD I]) (f : Polynomial R) : Polynomial.eval x f ≡ Polynomial.eval y f [SMOD I]

theorem SModEq.restrictScalars {R : Type u_1} [Ring R] (S : Type u_2) [Ring S] {M : Type u_4} [AddCommGroup M] [Module R M] [Module S M] {U : Submodule R M} {x y : M} [SMul S R] [IsScalarTower S R M] : x ≡ y [SMOD Submodule.restrictScalars S U] ↔ x ≡ y [SMOD U]

theorem SModEq.idealQuotientMk {R : Type u_6} [CommRing R] {I : Ideal R} {x y : R} : x ≡ y [SMOD I] ↔ (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y

@[simp]

theorem Submodule.vadd_set_subset_vadd_set_iff {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} : x +ᵥ ↑U ⊆ y +ᵥ ↑U ↔ x ≡ y [SMOD U]

@[simp]

theorem Submodule.vadd_set_eq_vadd_set_iff {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} : x +ᵥ ↑U = y +ᵥ ↑U ↔ x ≡ y [SMOD U]