Module operations on Mᵐᵒᵖ

This file contains definitions that build on top of the group action definitions in Mathlib.Algebra.GroupWithZero.Action.Opposite.

@[instance 910]

instance Semiring.toOppositeModule {R : Type u_1} [Semiring R] : Module Rᵐᵒᵖ R

Like Semiring.toModule, but multiplies on the right.

Equations

• Semiring.toOppositeModule = Module.mk ⋯ ⋯

instance MulOpposite.instModule (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : Module R Mᵐᵒᵖ

MulOpposite.distribMulAction extends to a Module

Equations

• MulOpposite.instModule R = Module.mk ⋯ ⋯