subtypeMop — Mathlib

English

Defines a linear map from I to Rᵐᵒᵖ by taking x ∈ I to MulOpposite.op x.1.

Русский

Определяет линейное отображение из I в Rᵐᵒᵖ, отправляющее x ∈ I в MulOpposite.op x.1.

LaTeX

$$def subtypeMop : I →ₗ[R^{\\mathrm{op}}] (R^{\\mathrm{op}})$$

Lean4

/-- For any `RingCon R`, when we view it as an ideal in `Rᵒᵖ`, `subtype` is the injective `Rᵐᵒᵖ`-linear
map `I → Rᵐᵒᵖ`.
-/
@[simps]
def subtypeMop : I →ₗ[Rᵐᵒᵖ] Rᵐᵒᵖ where
  toFun x := MulOpposite.op x.1
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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