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įµįµ’įµ–.

Equations
    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.

      Equations
        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įµįµ’įµ–.

          Equations
            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