instModule — Mathlib

English

From a given R-module M, the opposite Mᵐᵒᵖ inherits an R-module structure via unop; i.e. Mᵐᵒᵖ is a module over R with smul given by unop and opp.

Русский

Из модуля R над M получаем структуру модуля на противоположном объекте Mᵐᵒᵖ через unop; то есть Mᵐᵒᵖ является модулем над R.

LaTeX

$$$\\mathrm{Module}\\ R\\ M^{\\mathrm{op}}$$$

Lean4

/-- `MulOpposite.distribMulAction` extends to a `Module` -/
instance instModule : Module R Mᵐᵒᵖ
    where
  add_smul _ _ _ := unop_injective <| add_smul _ _ _
  zero_smul _ := unop_injective <| zero_smul _ _

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