unop — Mathlib

English

From a subring of the opposite ring Rᵐᵒᵖ one obtains a subring of R by unop.

Русский

Из подкольца противоположного кольца Rᵐᵒᵖ получается подкольцо R через unop.

LaTeX

$$$S^{\mathrm{unop}} \subseteq R \text{ is a Subring of } R$.$$

Lean4

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

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