ringEquivOpMop — Mathlib

English

There is a canonical ring isomorphism between the opposite of a subring S and the opposite of its subring S.op.

Русский

Существует канонический кольцевой изоморфизм между противоположностью подкольца S и противоположностью S.op.

LaTeX

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

Lean4

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

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