toOppositeModule — Mathlib

English

Like the usual module structure, but on the opposite multiplicative side, giving a Module Rᵐᵒᵖ on R with right action defined by reversal of multiplication.

Русский

Как обычная структура модуля, но на противоположной стороне умножения, образующая модуль Rᵐᵒᵖ над R с правым действием, заданным через обращение порядка умножения.

LaTeX

$$$\\text{Module } (MulOpposite R) R$$$

Lean4

/-- Like `Semiring.toModule`, but multiplies on the right. -/
instance (priority := 910) toOppositeModule [Semiring R] : Module Rᵐᵒᵖ R :=
  {
    MonoidWithZero.toOppositeMulActionWithZero
      R with
    smul_add := fun _ _ _ => add_mul _ _ _
    add_smul := fun _ _ _ => mul_add _ _ _ }

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