Documentation

Mathlib.LinearAlgebra.SModEq

modular equivalence for submodule #

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

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

Equations
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem SModEq.def {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} :
      theorem SModEq.sub_mem {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} :
      x y [SMOD U] x - y U
      @[simp]
      theorem SModEq.top {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {x : M} {y : M} :
      @[simp]
      theorem SModEq.bot {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {x : M} {y : M} :
      x y [SMOD ] x = y
      theorem SModEq.mono {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U₁ : Submodule R M} {U₂ : Submodule R M} {x : M} {y : M} (HU : U₁ U₂) (hxy : x y [SMOD U₁]) :
      x y [SMOD U₂]
      theorem SModEq.refl {R : Type u_1} [Ring R] {M : Type u_3} [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_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} :
      x x [SMOD U]
      instance SModEq.instIsRefl {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} :
      Equations
      • =
      theorem SModEq.symm {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} (hxy : x y [SMOD U]) :
      y x [SMOD U]
      theorem SModEq.trans {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} {z : M} (hxy : x y [SMOD U]) (hyz : y z [SMOD U]) :
      x z [SMOD U]
      instance SModEq.instTrans {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} :
      Equations
      • SModEq.instTrans = { trans := }
      theorem SModEq.add {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x₁ : M} {x₂ : M} {y₁ : M} {y₂ : M} (hxy₁ : x₁ y₁ [SMOD U]) (hxy₂ : x₂ y₂ [SMOD U]) :
      x₁ + x₂ y₁ + y₂ [SMOD U]
      theorem SModEq.smul {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {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_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {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_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} (hxy : x y [SMOD U]) (n : ) :
      n x n y [SMOD U]
      theorem SModEq.mul {A : Type u_2} [CommRing A] {I : Ideal A} {x₁ : A} {x₂ : A} {y₁ : A} {y₂ : A} (hxy₁ : x₁ y₁ [SMOD I]) (hxy₂ : x₂ y₂ [SMOD I]) :
      x₁ * x₂ y₁ * y₂ [SMOD I]
      theorem SModEq.pow {A : Type u_2} [CommRing A] {I : Ideal A} {x : A} {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_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} (hxy : x y [SMOD U]) :
      theorem SModEq.sub {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x₁ : M} {x₂ : M} {y₁ : M} {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_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} :
      x 0 [SMOD U] x U
      theorem SModEq.map {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} {N : Type u_4} [AddCommGroup N] [Module R N] (hxy : x y [SMOD U]) (f : M →ₗ[R] N) :
      theorem SModEq.comap {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {x : M} {y : M} {N : Type u_4} [AddCommGroup N] [Module R N] (V : Submodule R N) {f : M →ₗ[R] N} (hxy : f x f y [SMOD V]) :
      theorem SModEq.eval {R : Type u_5} [CommRing R] {I : Ideal R} {x : R} {y : R} (h : x y [SMOD I]) (f : Polynomial R) :