Module operations on Mᵐᵒᵖ #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains definitions that build on top of the group action definitions in
group_theory.group_action.opposite.
@[protected, instance]
mul_opposite.distrib_mul_action extends to a module
Equations
- mul_opposite.module R = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action (mul_opposite.distrib_mul_action M R), smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}
def
mul_opposite.op_linear_equiv
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M] :
The function op is a linear equivalence.
Equations
- mul_opposite.op_linear_equiv R = {to_fun := mul_opposite.op_add_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := mul_opposite.op_add_equiv.inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
mul_opposite.coe_op_linear_equiv
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M] :
@[simp]
theorem
mul_opposite.coe_op_linear_equiv_symm
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M] :
@[simp]
theorem
mul_opposite.coe_op_linear_equiv_to_linear_map
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M] :
@[simp]
theorem
mul_opposite.coe_op_linear_equiv_symm_to_linear_map
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M] :
@[simp]
theorem
mul_opposite.op_linear_equiv_to_add_equiv
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M] :
@[simp]
theorem
mul_opposite.op_linear_equiv_symm_to_add_equiv
(R : Type u)
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M] :