mathlib documentation

algebra.module.opposites

Module operations on Mᵐᵒᵖ #

This file contains definitions that build on top of the group action definitions in group_theory.group_action.opposite.

def mul_opposite.op_linear_equiv (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

The function op is a linear equivalence.

Equations