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 = { toMulAction := MulActionWithZero.toMulAction, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

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 = { toDistribMulAction := MulOpposite.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }