Documentation

Mathlib.Algebra.Ring.Subsemiring.MulOpposite

Subsemiring of opposite semirings #

For every semiring R, we construct an equivalence between subsemirings of R and that of Rᵐᵒᵖ.

Pull a subsemiring back to an opposite subsemiring along MulOpposite.unop

Equations
  • S.op = { toSubmonoid := S.op, add_mem' := , zero_mem' := }
Instances For

    Pull an opposite subsemiring back to a subsemiring along MulOpposite.op

    Equations
    • S.unop = { toSubmonoid := S.unop, add_mem' := , zero_mem' := }
    Instances For
      @[simp]

      Lattice results #

      @[simp]
      theorem Subsemiring.op_le_op_iff {R : Type u_2} [NonAssocSemiring R] {S₁ S₂ : Subsemiring R} :

      A subsemiring S of R determines a subsemiring S.op of the opposite ring Rᵐᵒᵖ.

      Equations
      Instances For
        @[simp]
        @[simp]
        theorem Subsemiring.op_inj {R : Type u_2} [NonAssocSemiring R] {S T : Subsemiring R} :
        @[simp]
        @[simp]
        theorem Subsemiring.op_sup {R : Type u_2} [NonAssocSemiring R] (S₁ S₂ : Subsemiring R) :
        (S₁ S₂).op = S₁.op S₂.op
        theorem Subsemiring.op_inf {R : Type u_2} [NonAssocSemiring R] (S₁ S₂ : Subsemiring R) :
        (S₁ S₂).op = S₁.op S₂.op
        theorem Subsemiring.op_iSup {ι : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ιSubsemiring R) :
        (iSup S).op = ⨆ (i : ι), (S i).op
        theorem Subsemiring.unop_iSup {ι : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ιSubsemiring Rᵐᵒᵖ) :
        (iSup S).unop = ⨆ (i : ι), (S i).unop
        theorem Subsemiring.op_iInf {ι : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ιSubsemiring R) :
        (iInf S).op = ⨅ (i : ι), (S i).op
        theorem Subsemiring.unop_iInf {ι : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ιSubsemiring Rᵐᵒᵖ) :
        (iInf S).unop = ⨅ (i : ι), (S i).unop

        Bijection between a subsemiring S and its opposite.

        Equations
        Instances For

          Bijection between a subsemiring S and MulOpposite of its opposite.

          Equations
          Instances For
            @[simp]

            Bijection between MulOpposite of a subsemiring S and its opposite.

            Equations
            Instances For