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) [AddMonoid R] [AddAction R α] (x : αᵃᵒᵖ) : 0 +ᵥ x = x

theorem AddOpposite.addAction.proof_2 (α : Type u_1) (R : Type u_2) [AddMonoid R] [AddAction R α] (r₁ : R) (r₂ : R) (x : αᵃᵒᵖ) : r₁ + r₂ +ᵥ x = r₁ +ᵥ (r₂ +ᵥ x)

instance AddOpposite.addAction (α : Type u_1) (R : Type u_2) [AddMonoid R] [AddAction R α] : AddAction R αᵃᵒᵖ

Equations

• AddOpposite.addAction α R = AddAction.mk (_ : ∀ (x : αᵃᵒᵖ), 0 +ᵥ x = x) (_ : ∀ (r₁ r₂ : R) (x : αᵃᵒᵖ), r₁ + r₂ +ᵥ x = r₁ +ᵥ (r₂ +ᵥ x))

instance MulOpposite.mulAction (α : Type u_1) (R : Type u_2) [Monoid R] [MulAction R α] : MulAction R αᵐᵒᵖ

Equations

• MulOpposite.mulAction α R = MulAction.mk (_ : ∀ (x : αᵐᵒᵖ), 1 • x = x) (_ : ∀ (r₁ r₂ : R) (x : αᵐᵒᵖ), (r₁ * r₂) • x = r₁ • r₂ • x)

instance MulOpposite.distribMulAction (α : Type u_1) (R : Type u_2) [Monoid R] [AddMonoid α] [DistribMulAction R α] : DistribMulAction R αᵐᵒᵖ

Equations

• MulOpposite.distribMulAction α R = DistribMulAction.mk (_ : ∀ (r : R), r • 0 = 0) (_ : ∀ (r : R) (x₁ x₂ : αᵐᵒᵖ), r • (x₁ + x₂) = r • x₁ + r • x₂)

instance MulOpposite.mulDistribMulAction (α : Type u_1) (R : Type u_2) [Monoid R] [Monoid α] [MulDistribMulAction R α] : MulDistribMulAction R αᵐᵒᵖ

Equations

• MulOpposite.mulDistribMulAction α R = MulDistribMulAction.mk (_ : ∀ (r : R) (x₁ x₂ : αᵐᵒᵖ), r • (x₁ * x₂) = r • x₁ * r • x₂) (_ : ∀ (r : R), r • 1 = 1)

theorem AddOpposite.isScalarTower.proof_1 (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M N] [VAdd M α] [VAdd N α] [VAddAssocClass M N α] : VAddAssocClass M N αᵃᵒᵖ

instance AddOpposite.isScalarTower (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M N] [VAdd M α] [VAdd N α] [VAddAssocClass M N α] : VAddAssocClass M N αᵃᵒᵖ

Equations

• AddOpposite.isScalarTower = AddOpposite.isScalarTower.proof_1

instance MulOpposite.isScalarTower (α : Type u_1) {M : Type u_2} {N : Type u_3} [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] : IsScalarTower M N αᵐᵒᵖ

Equations

• MulOpposite.isScalarTower = MulOpposite.isScalarTower.proof_1

instance AddOpposite.vaddCommClass (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] : VAddCommClass M N αᵃᵒᵖ

Equations

• AddOpposite.vaddCommClass = AddOpposite.vaddCommClass.proof_1

theorem AddOpposite.vaddCommClass.proof_1 (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] : VAddCommClass M N αᵃᵒᵖ

instance MulOpposite.smulCommClass (α : Type u_1) {M : Type u_2} {N : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass M N αᵐᵒᵖ

Equations

• MulOpposite.smulCommClass = MulOpposite.smulCommClass.proof_1

instance AddOpposite.isCentralVAdd (α : Type u_1) (R : Type u_2) [VAdd R α] [VAdd Rᵃᵒᵖ α] [IsCentralVAdd R α] : IsCentralVAdd R αᵃᵒᵖ

Equations

• AddOpposite.isCentralVAdd = AddOpposite.isCentralVAdd.proof_1

theorem AddOpposite.isCentralVAdd.proof_1 (α : Type u_1) (R : Type u_2) [VAdd R α] [VAdd Rᵃᵒᵖ α] [IsCentralVAdd R α] : IsCentralVAdd R αᵃᵒᵖ

instance MulOpposite.isCentralScalar (α : Type u_1) (R : Type u_2) [SMul R α] [SMul Rᵐᵒᵖ α] [IsCentralScalar R α] : IsCentralScalar R αᵐᵒᵖ

Equations

• MulOpposite.isCentralScalar = MulOpposite.isCentralScalar.proof_1

theorem MulOpposite.op_smul_eq_op_smul_op (α : Type u_1) {R : Type u_2} [SMul R α] [SMul Rᵐᵒᵖ α] [IsCentralScalar R α] (r : R) (a : α) : MulOpposite.op (r • a) = MulOpposite.op r • MulOpposite.op a

theorem MulOpposite.unop_smul_eq_unop_smul_unop (α : Type u_1) {R : Type u_2} [SMul R α] [SMul Rᵐᵒᵖ α] [IsCentralScalar R α] (r : Rᵐᵒᵖ) (a : αᵐᵒᵖ) : MulOpposite.unop (r • a) = MulOpposite.unop r • MulOpposite.unop 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.

instance Add.toHasOppositeVAdd (α : Type u_1) [Add α] : VAdd αᵃᵒᵖ α

Like Add.toVAdd, but adds on the right.

See also AddMonoid.to_OppositeAddAction.

Equations

• Add.toHasOppositeVAdd α = { vadd := fun c x => x + AddOpposite.unop c }

instance Mul.toHasOppositeSMul (α : Type u_1) [Mul α] : SMul αᵐᵒᵖ α

Like Mul.toSMul, but multiplies on the right.

See also Monoid.toOppositeMulAction and MonoidWithZero.toOppositeMulActionWithZero.

Equations

• Mul.toHasOppositeSMul α = { smul := fun c x => x * MulOpposite.unop c }

theorem op_vadd_eq_add (α : Type u_1) [Add α] {a : α} {a' : α} : AddOpposite.op a +ᵥ a' = a' + a

theorem op_smul_eq_mul (α : Type u_1) [Mul α] {a : α} {a' : α} : MulOpposite.op a • a' = a' * a

@[simp]

theorem AddOpposite.vadd_eq_add_unop (α : Type u_1) [Add α] {a : αᵃᵒᵖ} {a' : α} : a +ᵥ a' = a' + AddOpposite.unop a

@[simp]

theorem MulOpposite.smul_eq_mul_unop (α : Type u_1) [Mul α] {a : αᵐᵒᵖ} {a' : α} : a • a' = a' * MulOpposite.unop a

theorem AddAction.OppositeRegular.isPretransitive.proof_1 {G : Type u_1} [AddGroup G] : AddAction.IsPretransitive Gᵃᵒᵖ G

instance AddAction.OppositeRegular.isPretransitive {G : Type u_2} [AddGroup G] : AddAction.IsPretransitive Gᵃᵒᵖ G

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

Equations

• @AddAction.OppositeRegular.isPretransitive = @AddAction.OppositeRegular.isPretransitive.proof_1

instance MulAction.OppositeRegular.isPretransitive {G : Type u_2} [Group G] : MulAction.IsPretransitive Gᵐᵒᵖ G

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

Equations

• @MulAction.OppositeRegular.isPretransitive = @MulAction.OppositeRegular.isPretransitive.proof_1

instance AddSemigroup.opposite_vaddCommClass (α : Type u_1) [AddSemigroup α] : VAddCommClass αᵃᵒᵖ α α

Equations

• AddSemigroup.opposite_vaddCommClass = AddSemigroup.opposite_vaddCommClass.proof_1

theorem AddSemigroup.opposite_vaddCommClass.proof_1 (α : Type u_1) [AddSemigroup α] : VAddCommClass αᵃᵒᵖ α α

instance Semigroup.opposite_smulCommClass (α : Type u_1) [Semigroup α] : SMulCommClass αᵐᵒᵖ α α

Equations

• Semigroup.opposite_smulCommClass = Semigroup.opposite_smulCommClass.proof_1

instance AddSemigroup.opposite_vaddCommClass' (α : Type u_1) [AddSemigroup α] : VAddCommClass α αᵃᵒᵖ α

Equations

• AddSemigroup.opposite_vaddCommClass' = AddSemigroup.opposite_vaddCommClass'.proof_1

theorem AddSemigroup.opposite_vaddCommClass'.proof_1 (α : Type u_1) [AddSemigroup α] : VAddCommClass α αᵃᵒᵖ α

instance Semigroup.opposite_smulCommClass' (α : Type u_1) [Semigroup α] : SMulCommClass α αᵐᵒᵖ α

Equations

• Semigroup.opposite_smulCommClass' = Semigroup.opposite_smulCommClass'.proof_1

instance AddCommSemigroup.isCentralVAdd (α : Type u_1) [AddCommSemigroup α] : IsCentralVAdd α α

Equations

• AddCommSemigroup.isCentralVAdd = AddCommSemigroup.isCentralVAdd.proof_1

theorem AddCommSemigroup.isCentralVAdd.proof_1 (α : Type u_1) [AddCommSemigroup α] : IsCentralVAdd α α

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

Equations

• CommSemigroup.isCentralScalar = CommSemigroup.isCentralScalar.proof_1

instance AddMonoid.toOppositeAddAction (α : Type u_1) [AddMonoid α] : AddAction αᵃᵒᵖ α

Like AddMonoid.toAddAction, but adds on the right.

Equations

• One or more equations did not get rendered due to their size.

theorem AddMonoid.toOppositeAddAction.proof_2 (α : Type u_1) [AddMonoid α] : ∀ (x x_1 : αᵃᵒᵖ) (x_2 : α), x_2 + (AddOpposite.unop x_1 + AddOpposite.unop x) = x_2 + AddOpposite.unop x_1 + AddOpposite.unop x

theorem AddMonoid.toOppositeAddAction.proof_1 (α : Type u_1) [AddMonoid α] (a : α) : a + 0 = a

instance Monoid.toOppositeMulAction (α : Type u_1) [Monoid α] : MulAction αᵐᵒᵖ α

Like Monoid.toMulAction, but multiplies on the right.

Equations

• One or more equations did not get rendered due to their size.

theorem VAddAssocClass.opposite_mid.proof_1 {M : Type u_1} {N : Type u_2} [Add N] [VAdd M N] [VAddCommClass M N N] : VAddAssocClass M Nᵃᵒᵖ N

instance VAddAssocClass.opposite_mid {M : Type u_2} {N : Type u_3} [Add N] [VAdd M N] [VAddCommClass M N N] : VAddAssocClass M Nᵃᵒᵖ N

Equations

• @VAddAssocClass.opposite_mid = @VAddAssocClass.opposite_mid.proof_1

instance IsScalarTower.opposite_mid {M : Type u_2} {N : Type u_3} [Mul N] [SMul M N] [SMulCommClass M N N] : IsScalarTower M Nᵐᵒᵖ N

Equations

• @IsScalarTower.opposite_mid = @IsScalarTower.opposite_mid.proof_1

theorem VAddCommClass.opposite_mid.proof_1 {M : Type u_1} {N : Type u_2} [Add N] [VAdd M N] [VAddAssocClass M N N] : VAddCommClass M Nᵃᵒᵖ N

instance VAddCommClass.opposite_mid {M : Type u_2} {N : Type u_3} [Add N] [VAdd M N] [VAddAssocClass M N N] : VAddCommClass M Nᵃᵒᵖ N

Equations

• @VAddCommClass.opposite_mid = @VAddCommClass.opposite_mid.proof_1

instance SMulCommClass.opposite_mid {M : Type u_2} {N : Type u_3} [Mul N] [SMul M N] [IsScalarTower M N N] : SMulCommClass M Nᵐᵒᵖ N

Equations

• @SMulCommClass.opposite_mid = @SMulCommClass.opposite_mid.proof_1

instance AddLeftCancelMonoid.toFaithfulVAdd_opposite (α : Type u_1) [AddLeftCancelMonoid α] : FaithfulVAdd αᵃᵒᵖ α

AddMonoid.toOppositeAddAction is faithful on cancellative monoids.

Equations

• AddLeftCancelMonoid.toFaithfulVAdd_opposite = AddLeftCancelMonoid.toFaithfulVAdd_opposite.proof_1

theorem AddLeftCancelMonoid.toFaithfulVAdd_opposite.proof_1 (α : Type u_1) [AddLeftCancelMonoid α] : FaithfulVAdd αᵃᵒᵖ α

instance LeftCancelMonoid.toFaithfulSMul_opposite (α : Type u_1) [LeftCancelMonoid α] : FaithfulSMul αᵐᵒᵖ α

Monoid.toOppositeMulAction is faithful on cancellative monoids.

Equations

• LeftCancelMonoid.toFaithfulSMul_opposite = LeftCancelMonoid.toFaithfulSMul_opposite.proof_1

instance CancelMonoidWithZero.toFaithfulSMul_opposite (α : Type u_1) [CancelMonoidWithZero α] [Nontrivial α] : FaithfulSMul αᵐᵒᵖ α

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

Equations

• CancelMonoidWithZero.toFaithfulSMul_opposite = CancelMonoidWithZero.toFaithfulSMul_opposite.proof_1