Documentation

Mathlib.Algebra.Module.Opposites

Module operations on Mᵐᵒᵖ #

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

instance MulOpposite.instModule (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

MulOpposite.distribMulAction extends to a Module

Equations

The function op is a linear equivalence.

Equations
  • MulOpposite.opLinearEquiv R = { toFun := MulOpposite.opAddEquiv.toFun, map_add' := , map_smul' := , invFun := MulOpposite.opAddEquiv.invFun, left_inv := , right_inv := }
Instances For
    @[simp]
    theorem MulOpposite.coe_opLinearEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    (MulOpposite.opLinearEquiv R) = MulOpposite.op
    @[simp]
    theorem MulOpposite.coe_opLinearEquiv_symm (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    (MulOpposite.opLinearEquiv R).symm = MulOpposite.unop
    @[simp]
    theorem MulOpposite.coe_opLinearEquiv_toLinearMap (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    (MulOpposite.opLinearEquiv R) = MulOpposite.op
    @[simp]
    theorem MulOpposite.coe_opLinearEquiv_symm_toLinearMap (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    (MulOpposite.opLinearEquiv R).symm = MulOpposite.unop
    theorem MulOpposite.opLinearEquiv_toAddEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    (MulOpposite.opLinearEquiv R).toAddEquiv = MulOpposite.opAddEquiv
    @[simp]
    theorem MulOpposite.coe_opLinearEquiv_addEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    (MulOpposite.opLinearEquiv R) = MulOpposite.opAddEquiv
    theorem MulOpposite.opLinearEquiv_symm_toAddEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    (MulOpposite.opLinearEquiv R).symm.toAddEquiv = MulOpposite.opAddEquiv.symm
    @[simp]
    theorem MulOpposite.coe_opLinearEquiv_symm_addEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
    (MulOpposite.opLinearEquiv R).symm = MulOpposite.opAddEquiv.symm