# Module operations on `Mᵐᵒᵖ` #

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

source
theorem LinearMap.ext_ring_op {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module S M] {σ : R ᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M} (h : f 1 = g 1) :
f = g
source
theorem LinearMap.ext_ring_op_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module S M] {σ : R ᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M} :
f = g ↔ f 1 = g 1
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

- MulOpposite.opLinearEquiv R = { toFun := MulOpposite.opAddEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := MulOpposite.opAddEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem MulOpposite.coe_opLinearEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
⇑(opLinearEquiv R) = op
source
@[simp]
theorem MulOpposite.coe_opLinearEquiv_symm (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
⇑(opLinearEquiv R).symm = unop
source
@[simp]
theorem MulOpposite.coe_opLinearEquiv_toLinearMap (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
⇑↑(opLinearEquiv R) = op
source
@[simp]
theorem MulOpposite.coe_opLinearEquiv_symm_toLinearMap (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
⇑↑(opLinearEquiv R).symm = unop
source
theorem MulOpposite.opLinearEquiv_toAddEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
(opLinearEquiv R).toAddEquiv = opAddEquiv
source
@[simp]
theorem MulOpposite.coe_opLinearEquiv_addEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
↑(opLinearEquiv R) = opAddEquiv
source
theorem MulOpposite.opLinearEquiv_symm_toAddEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
(opLinearEquiv R).symm.toAddEquiv = opAddEquiv.symm
source
@[simp]
theorem MulOpposite.coe_opLinearEquiv_symm_addEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
↑(opLinearEquiv R).symm = opAddEquiv.symm