Module operations on Mᵒᵖ #
This file contains definitions that could not be placed into algebra.opposites due to import
cycles.
@[instance]
def
opposite.semimodule
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
semimodule R Mᵒᵖ
opposite.distrib_mul_action extends to a semimodule
Equations
- opposite.semimodule R = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action (opposite.distrib_mul_action M R), smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
def
opposite.op_linear_equiv
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
The function op is a linear equivalence.
Equations
- opposite.op_linear_equiv R = {to_fun := opposite.op_add_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := opposite.op_add_equiv.inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
opposite.coe_op_linear_equiv
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
@[simp]
theorem
opposite.coe_op_linear_equiv_symm
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
@[simp]
theorem
opposite.coe_op_linear_equiv_to_linear_map
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
@[simp]
theorem
opposite.coe_op_linear_equiv_symm_to_linear_map
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
@[simp]
theorem
opposite.op_linear_equiv_to_add_equiv
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
@[simp]
theorem
opposite.op_linear_equiv_symm_to_add_equiv
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :