mathlib documentation

algebra.module.opposites

Module operations on Mᵒᵖ #

This file contains definitions that could not be placed into algebra.opposites due to import cycles.

def 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
@[simp]