op — Mathlib · SciLib

English

There is a Subring of the opposite ring Rᵐᵒᵖ consisting of the same elements with reversed multiplication.

Русский

Существует подкольцо противоположного кольца Rᵐᵒᵖ, содержащее те же элементы, но с обращенной умножением.

LaTeX

$$$S\mapsto S^{\mathrm{op}} \,\text{is a Subring of } R^{\mathrm{op}},\; \text{with } x\in S^{\mathrm{op}} \iff x^{\mathrm{unop}}\in S.$$$

Lean4

/-- Pull a subring back to an opposite subring along `MulOpposite.unop` -/
@[simps! coe toSubsemiring]
protected def op (S : Subring R) : Subring Rᵐᵒᵖ
    where
  toSubsemiring := S.toSubsemiring.op
  neg_mem' {x} hx := neg_mem (show x.unop ∈ S from hx)

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