mopRingEquivOp — Mathlib

English

There is a ring isomorphism between the opposite of a subring S and the opposite of its opposite, i.e., Sᵐᵒᵖ ≃+* (S.op).

Русский

Существует кольцевой изоморфизм между противоположностью подкольца S и противоположностью самой противоположности, т.е. Sᵐᵒᵖ ≃+* (S.op).

LaTeX

$$$S^{\mathrm{op}} \cong_{\text{ring}} (S^{\mathrm{op}})^{\mathrm{op}}$$$

Lean4

/-- Bijection between `MulOpposite` of a subring `S` and its opposite. -/
@[simps!]
def mopRingEquivOp (S : Subring R) : Sᵐᵒᵖ ≃+* S.op :=
  S.toSubsemiring.mopRingEquivOp

Похожие утверждения