Theorems · Definition · linear algebra

Submodule.quotientRel

{R : Type u_1} →
  {M : Type u_2} → [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Submodule R M → Setoid M

The equivalence relation associated to a submodule p, defined by x ≈ y iff -x + y ∈ p. Note this is equivalent to y - x ∈ p, but defined this way to be defeq to the AddSubgroup version, where commutativity can't be assumed.

Defined in

Mathlib.LinearAlgebra.Quotient.Defs

Cited by

18 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModule