Documentation

Mathlib.Algebra.Module.Opposites

Module operations on Mᵐᵒᵖ #

This file contains definitions that build on top of the group action definitions in GroupTheory.GroupAction.Opposite.

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
source
def MulOpposite.opLinearEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
M ≃ₗ[R] Mᵐᵒᵖ

The function op is a linear equivalence.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem MulOpposite.coe_opLinearEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    ⇑(MulOpposite.opLinearEquiv R) = MulOpposite.op
    source
    @[simp]
    theorem MulOpposite.coe_opLinearEquiv_symm (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    ⇑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) = MulOpposite.unop
    source
    @[simp]
    theorem MulOpposite.coe_opLinearEquiv_toLinearMap (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    ⇑↑(MulOpposite.opLinearEquiv R) = MulOpposite.op
    source
    @[simp]
    theorem MulOpposite.coe_opLinearEquiv_symm_toLinearMap (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    ⇑↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) = MulOpposite.unop
    source
    theorem MulOpposite.opLinearEquiv_toAddEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    LinearEquiv.toAddEquiv (MulOpposite.opLinearEquiv R) = MulOpposite.opAddEquiv
    source
    @[simp]
    theorem MulOpposite.coe_opLinearEquiv_addEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    ↑(MulOpposite.opLinearEquiv R) = MulOpposite.opAddEquiv
    source
    theorem MulOpposite.opLinearEquiv_symm_toAddEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    LinearEquiv.toAddEquiv (LinearEquiv.symm (MulOpposite.opLinearEquiv R)) = AddEquiv.symm MulOpposite.opAddEquiv
    source
    @[simp]
    theorem MulOpposite.coe_opLinearEquiv_symm_addEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    ↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) = AddEquiv.symm MulOpposite.opAddEquiv