Module operations on Mᵐᵒᵖ

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

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

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

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.

@[simp]

theorem MulOpposite.coe_opLinearEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : ⇑(opLinearEquiv R) = op

@[simp]

theorem MulOpposite.coe_opLinearEquiv_symm (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : ⇑(opLinearEquiv R).symm = unop

@[simp]

theorem MulOpposite.coe_opLinearEquiv_toLinearMap (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : ⇑↑(opLinearEquiv R) = op

@[simp]

theorem MulOpposite.coe_opLinearEquiv_symm_toLinearMap (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : ⇑↑(opLinearEquiv R).symm = unop

theorem MulOpposite.opLinearEquiv_toAddEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : (opLinearEquiv R).toAddEquiv = opAddEquiv

@[simp]

theorem MulOpposite.coe_opLinearEquiv_addEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : ↑(opLinearEquiv R) = opAddEquiv

theorem MulOpposite.opLinearEquiv_symm_toAddEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : (opLinearEquiv R).symm.toAddEquiv = opAddEquiv.symm

@[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