op — Mathlib · SciLib

English

For any subalgebra S ⊆ A, the subalgebra S.op is a subalgebra of the opposite ring Aᵐᵒᵖ.

Русский

Для любой подалгебры S ⊆ A, подалгебра S.op является подалгеброй над противоположным кольцом Aᵐᵒᵖ.

LaTeX

$$$ S^{\mathrm{op}} \\text{is a subalgebra of } A^{\mathrm{op}}. $$$

Lean4

/-- Pull a subalgebra back to an opposite subalgebra along `MulOpposite.unop` -/
@[simps! coe toSubsemiring]
protected def op (S : Subalgebra R A) : Subalgebra R Aᵐᵒᵖ
    where
  toSubsemiring := S.toSubsemiring.op
  algebraMap_mem' := S.algebraMap_mem

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