Documentation

Mathlib.Algebra.Module.Opposites

Module operations on Mᵐᵒᵖ #

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

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

MulOpposite.distribMulAction extends to a Module

Equations
def MulOpposite.opLinearEquiv (R : Type u) {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :

The function op is a linear equivalence.

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