Actions by and on order synonyms

This PR transfers group action with zero instances from a type α to αᵒᵈ and Lex α. Note that the SMul instances are already defined in Mathlib/Algebra/Order/Group/Synonym.lean.

See also

• Mathlib/Algebra/Order/Group/Action/Synonym.lean
• Mathlib/Algebra/Order/Module/Synonym.lean

@[implicit_reducible]

instance OrderDual.instSMulZeroClass {G₀ : Type u_1} {M₀ : Type u_2} [Zero M₀] [h : SMulZeroClass G₀ M₀] : SMulZeroClass G₀ᵒᵈ M₀

Equations

• OrderDual.instSMulZeroClass = { toSMul := OrderDual.instSMul', smul_zero := ⋯ }

@[implicit_reducible]

instance OrderDual.instSMulZeroClass_1 {G₀ : Type u_1} {M₀ : Type u_2} [Zero M₀] [h : SMulZeroClass G₀ M₀] : SMulZeroClass G₀ M₀ᵒᵈ

Equations

• OrderDual.instSMulZeroClass_1 = { toSMul := OrderDual.instSMul, smul_zero := ⋯ }

@[implicit_reducible]

instance OrderDual.instSMulWithZero {G₀ : Type u_1} {M₀ : Type u_2} [Zero G₀] [Zero M₀] [h : SMulWithZero G₀ M₀] : SMulWithZero G₀ᵒᵈ M₀

Equations

• OrderDual.instSMulWithZero = { toSMulZeroClass := OrderDual.instSMulZeroClass, zero_smul := ⋯ }

@[implicit_reducible]

instance OrderDual.instSMulWithZero_1 {G₀ : Type u_1} {M₀ : Type u_2} [Zero G₀] [Zero M₀] [h : SMulWithZero G₀ M₀] : SMulWithZero G₀ M₀ᵒᵈ

Equations

• OrderDual.instSMulWithZero_1 = { toSMulZeroClass := OrderDual.instSMulZeroClass_1, zero_smul := ⋯ }

@[implicit_reducible]

instance OrderDual.instDistribSMul {G₀ : Type u_1} {M₀ : Type u_2} [AddZeroClass M₀] [h : DistribSMul G₀ M₀] : DistribSMul G₀ᵒᵈ M₀

Equations

• OrderDual.instDistribSMul = { toSMulZeroClass := OrderDual.instSMulZeroClass, smul_add := ⋯ }

@[implicit_reducible]

instance OrderDual.instDistribSMul_1 {G₀ : Type u_1} {M₀ : Type u_2} [AddZeroClass M₀] [h : DistribSMul G₀ M₀] : DistribSMul G₀ M₀ᵒᵈ

Equations

• OrderDual.instDistribSMul_1 = { toSMulZeroClass := OrderDual.instSMulZeroClass_1, smul_add := ⋯ }

@[implicit_reducible]

instance OrderDual.instDistribMulAction {G₀ : Type u_1} {M₀ : Type u_2} [Monoid G₀] [AddMonoid M₀] [h : DistribMulAction G₀ M₀] : DistribMulAction G₀ᵒᵈ M₀

Equations

• OrderDual.instDistribMulAction = { toMulAction := OrderDual.instMulAction, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

instance OrderDual.instDistribMulAction_1 {G₀ : Type u_1} {M₀ : Type u_2} [Monoid G₀] [AddMonoid M₀] [h : DistribMulAction G₀ M₀] : DistribMulAction G₀ M₀ᵒᵈ

Equations

• OrderDual.instDistribMulAction_1 = { toMulAction := OrderDual.instMulAction_1, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

instance OrderDual.instMulActionWithZero {G₀ : Type u_1} {M₀ : Type u_2} [MonoidWithZero G₀] [AddMonoid M₀] [h : MulActionWithZero G₀ M₀] : MulActionWithZero G₀ᵒᵈ M₀

Equations

• OrderDual.instMulActionWithZero = { toMulAction := OrderDual.instMulAction, smul_zero := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

instance OrderDual.instMulActionWithZero_1 {G₀ : Type u_1} {M₀ : Type u_2} [MonoidWithZero G₀] [AddMonoid M₀] [h : MulActionWithZero G₀ M₀] : MulActionWithZero G₀ M₀ᵒᵈ

Equations

• OrderDual.instMulActionWithZero_1 = { toMulAction := OrderDual.instMulAction_1, smul_zero := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

instance Lex.instSMulWithZero {G₀ : Type u_1} {M₀ : Type u_2} [Zero G₀] [Zero M₀] [SMulWithZero G₀ M₀] : SMulWithZero (Lex G₀) M₀

Equations

• Lex.instSMulWithZero = inst✝

@[implicit_reducible]

instance Lex.instSMulWithZero' {G₀ : Type u_1} {M₀ : Type u_2} [Zero G₀] [Zero M₀] [SMulWithZero G₀ M₀] : SMulWithZero G₀ (Lex M₀)

Equations

• Lex.instSMulWithZero' = inst✝

@[implicit_reducible]

instance Lex.instDistribSMul {G₀ : Type u_1} {M₀ : Type u_2} [AddZeroClass M₀] [DistribSMul G₀ M₀] : DistribSMul (Lex G₀) M₀

Equations

• Lex.instDistribSMul = inst✝

@[implicit_reducible]

instance Lex.instDistribSMul' {G₀ : Type u_1} {M₀ : Type u_2} [AddZeroClass M₀] [DistribSMul G₀ M₀] : DistribSMul G₀ (Lex M₀)

Equations

• Lex.instDistribSMul' = inst✝

@[implicit_reducible]

instance Lex.instDistribMulAction {G₀ : Type u_1} {M₀ : Type u_2} [Monoid G₀] [AddMonoid M₀] [DistribMulAction G₀ M₀] : DistribMulAction (Lex G₀) M₀

Equations

• Lex.instDistribMulAction = inst✝

@[implicit_reducible]

instance Lex.instDistribMulAction' {G₀ : Type u_1} {M₀ : Type u_2} [Monoid G₀] [AddMonoid M₀] [DistribMulAction G₀ M₀] : DistribMulAction G₀ (Lex M₀)

Equations

• Lex.instDistribMulAction' = inst✝

@[implicit_reducible]

instance Lex.instMulActionWithZero {G₀ : Type u_1} {M₀ : Type u_2} [MonoidWithZero G₀] [AddMonoid M₀] [MulActionWithZero G₀ M₀] : MulActionWithZero (Lex G₀) M₀

Equations

• Lex.instMulActionWithZero = inst✝

@[implicit_reducible]

instance Lex.instMulActionWithZero' {G₀ : Type u_1} {M₀ : Type u_2} [MonoidWithZero G₀] [AddMonoid M₀] [MulActionWithZero G₀ M₀] : MulActionWithZero G₀ (Lex M₀)

Equations

• Lex.instMulActionWithZero' = inst✝