unop — Mathlib

English

Pull a subalgebra from Aᵐᵒᵖ back to A by applying unop to its elements; i.e. unop maps Subalgebra R Aᵐᵒᵖ to Subalgebra R A.

Русский

Переносим подалгебру из A^{op} в A через применение unop; то есть unop отображает Subalgebra R A^{op} в Subalgebra R A.

LaTeX

$$$ \mathrm{unop}: \mathrm{Subalgebra}(R, A^{\mathrm{op}}) \to \mathrm{Subalgebra}(R, A) $$$

Lean4

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

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