# Documentation

Mathlib.GroupTheory.GroupAction.Opposite

# Scalar actions on and by Mᵐᵒᵖ#

This file defines the actions on the opposite type SMul R Mᵐᵒᵖ, and actions by the opposite type, SMul Rᵐᵒᵖ M.

Note that MulOpposite.smul is provided in an earlier file as it is needed to provide the AddMonoid.nsmul and AddCommGroup.zsmul fields.

### Actions on the opposite type #

Actions on the opposite type just act on the underlying type.

theorem AddOpposite.addAction.proof_1 (α : Type u_1) (R : Type u_2) [] [] (x : αᵃᵒᵖ) :
0 +ᵥ x = x
theorem AddOpposite.addAction.proof_2 (α : Type u_1) (R : Type u_2) [] [] (r₁ : R) (r₂ : R) (x : αᵃᵒᵖ) :
r₁ + r₂ +ᵥ x = r₁ +ᵥ (r₂ +ᵥ x)
instance AddOpposite.addAction (α : Type u_1) (R : Type u_2) [] [] :
instance MulOpposite.mulAction (α : Type u_1) (R : Type u_2) [] [] :
instance MulOpposite.distribMulAction (α : Type u_1) (R : Type u_2) [] [] [] :
instance MulOpposite.mulDistribMulAction (α : Type u_1) (R : Type u_2) [] [] [] :
theorem AddOpposite.isScalarTower.proof_1 (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M N] [VAdd M α] [VAdd N α] [] :
instance AddOpposite.isScalarTower (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M N] [VAdd M α] [VAdd N α] [] :
instance MulOpposite.isScalarTower (α : Type u_1) {M : Type u_2} {N : Type u_3} [SMul M N] [SMul M α] [SMul N α] [] :
instance MulOpposite.smulCommClass (α : Type u_1) {M : Type u_2} {N : Type u_3} [SMul M α] [SMul N α] [] :
instance MulOpposite.isCentralScalar (α : Type u_1) (R : Type u_2) [SMul R α] [SMul Rᵐᵒᵖ α] [] :
theorem MulOpposite.op_smul_eq_op_smul_op (α : Type u_1) {R : Type u_2} [SMul R α] [SMul Rᵐᵒᵖ α] [] (r : R) (a : α) :
theorem MulOpposite.unop_smul_eq_unop_smul_unop (α : Type u_1) {R : Type u_2} [SMul R α] [SMul Rᵐᵒᵖ α] [] (r : Rᵐᵒᵖ) (a : αᵐᵒᵖ) :

### Actions by the opposite type (right actions) #

In Mul.toSMul in another file, we define the left action a₁ • a₂ = a₁ * a₂. For the multiplicative opposite, we define MulOpposite.op a₁ • a₂ = a₂ * a₁, with the multiplication reversed.

Like Add.toVAdd, but adds on the right.

See also AddMonoid.to_OppositeAddAction.

instance Mul.toHasOppositeSMul (α : Type u_1) [Mul α] :

Like Mul.toSMul, but multiplies on the right.

See also Monoid.toOppositeMulAction and MonoidWithZero.toOppositeMulActionWithZero.

+ᵥ a' = a' + a
theorem op_smul_eq_mul (α : Type u_1) [Mul α] {a : α} {a' : α} :
a' = a' * a
@[simp]
a +ᵥ a' =
@[simp]
theorem MulOpposite.smul_eq_mul_unop (α : Type u_1) [Mul α] {a : αᵐᵒᵖ} {a' : α} :
a a' =

The right regular action of an additive group on itself is transitive.

The right regular action of a group on itself is transitive.

instance CommSemigroup.isCentralScalar (α : Type u_1) [] :

Like AddMonoid.toAddAction, but adds on the right.

∀ (x x_1 : αᵃᵒᵖ) (x_2 : α), x_2 + () = x_2 + +
a + 0 = a
instance Monoid.toOppositeMulAction (α : Type u_1) [] :

Like Monoid.toMulAction, but multiplies on the right.

theorem VAddAssocClass.opposite_mid.proof_1 {M : Type u_1} {N : Type u_2} [Add N] [VAdd M N] [] :
instance VAddAssocClass.opposite_mid {M : Type u_2} {N : Type u_3} [Add N] [VAdd M N] [] :
instance IsScalarTower.opposite_mid {M : Type u_2} {N : Type u_3} [Mul N] [SMul M N] [] :
theorem VAddCommClass.opposite_mid.proof_1 {M : Type u_1} {N : Type u_2} [Add N] [VAdd M N] [] :
instance VAddCommClass.opposite_mid {M : Type u_2} {N : Type u_3} [Add N] [VAdd M N] [] :
instance SMulCommClass.opposite_mid {M : Type u_2} {N : Type u_3} [Mul N] [SMul M N] [] :

AddMonoid.toOppositeAddAction is faithful on cancellative monoids.

Monoid.toOppositeMulAction is faithful on cancellative monoids.

Monoid.toOppositeMulAction is faithful on nontrivial cancellative monoids with zero.