Documentation

Mathlib.Algebra.Module.Opposite

Module operations on Mᵐᵒᵖ #

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

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

Like Semiring.toModule, but multiplies on the right.

Equations
    source
    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