algEquivOpMop — Mathlib

English

There is an algebra isomorphism between a subalgebra S and the opposite of its opposite: S ≃ₐ[R] (S.op)ᵐᵒᵖ.

Русский

Существует алгебраическое изоморождение между подалгеброй S и противоположностью противоположности S: S ≃ₐ[R] (S.op)ᵐᵒᵖ.

LaTeX

$$$$S \\cong_R (S^{op})^{op}$$$$

Lean4

/-- Bijection between a subalgebra `S` and `MulOpposite` of its opposite. -/
@[simps!]
def algEquivOpMop (S : Subalgebra R A) : S ≃ₐ[R] (S.op)ᵐᵒᵖ
    where
  __ := S.toSubsemiring.ringEquivOpMop
  commutes' _ := rfl

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