Documentation

Mathlib.RingTheory.Congruence.Opposite

Congruences on the opposite ring #

This file defines the order isomorphism between the congruences on a ring R and the congruences on the opposite ring Rįµįµ’įµ–.

source
šŸ”ø coverage
def RingCon.op {R : Type u_1} [Add R] [Mul R] (c : RingCon R) :
RingCon Rįµįµ’įµ–

If c is a RingCon R, then (a, b) ā†¦ c b.unop a.unop is a RingCon Rįµįµ’įµ–.

Instances For
    source
    šŸ“ coverage
    theorem RingCon.op_iff {R : Type u_1} [Add R] [Mul R] {c : RingCon R} {x y : Rįµįµ’įµ–} :
    c.op x y ā†” c (MulOpposite.unop y) (MulOpposite.unop x)
    source
    šŸ”ø coverage
    def RingCon.unop {R : Type u_1} [Add R] [Mul R] (c : RingCon Rįµįµ’įµ–) :
    RingCon R

    If c is a RingCon Rįµįµ’įµ–, then (a, b) ā†¦ c b.op a.op is a RingCon R.

    Instances For
      source
      šŸ“ coverage
      theorem RingCon.unop_iff {R : Type u_1} [Add R] [Mul R] {c : RingCon Rįµįµ’įµ–} {x y : R} :
      c.unop x y ā†” c (MulOpposite.op y) (MulOpposite.op x)
      source
      šŸ”ø coverage
      def RingCon.opOrderIso {R : Type u_1} [Add R] [Mul R] :
      RingCon R ā‰ƒo RingCon Rįµįµ’įµ–

      The congruences of a ring R biject to the congruences of the opposite ring Rįµįµ’įµ–.

      Instances For
        source
        šŸ“ coverage
        @[simp]
        theorem RingCon.opOrderIso_apply {R : Type u_1} [Add R] [Mul R] (c : RingCon R) :
        opOrderIso c = c.op
        source
        šŸ“ coverage
        @[simp]
        theorem RingCon.opOrderIso_symm_apply {R : Type u_1} [Add R] [Mul R] (c : RingCon Rįµįµ’įµ–) :
        (RelIso.symm opOrderIso) c = c.unop