Documentation

Mathlib.Algebra.Order.GroupWithZero.Action.Synonym

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 #

source
🔸 coverage
@[implicit_reducible]
instance OrderDual.instSMulZeroClass {G₀ : Type u_1} {M₀ : Type u_2} [Zero M₀] [h : SMulZeroClass G₀ M₀] :
SMulZeroClass G₀ᵒᵈ M₀
source
🔸 coverage
@[implicit_reducible]
instance OrderDual.instSMulZeroClass_1 {G₀ : Type u_1} {M₀ : Type u_2} [Zero M₀] [h : SMulZeroClass G₀ M₀] :
SMulZeroClass G₀ M₀ᵒᵈ
source
🔸 coverage
@[implicit_reducible]
instance OrderDual.instSMulWithZero {G₀ : Type u_1} {M₀ : Type u_2} [Zero G₀] [Zero M₀] [h : SMulWithZero G₀ M₀] :
SMulWithZero G₀ᵒᵈ M₀
source
🔸 coverage
@[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₀ᵒᵈ
source
🔸 coverage
@[implicit_reducible]
instance OrderDual.instDistribSMul {G₀ : Type u_1} {M₀ : Type u_2} [AddZeroClass M₀] [h : DistribSMul G₀ M₀] :
DistribSMul G₀ᵒᵈ M₀
source
🔸 coverage
@[implicit_reducible]
instance OrderDual.instDistribSMul_1 {G₀ : Type u_1} {M₀ : Type u_2} [AddZeroClass M₀] [h : DistribSMul G₀ M₀] :
DistribSMul G₀ M₀ᵒᵈ
source
🔸 coverage
@[implicit_reducible]
instance OrderDual.instDistribMulAction {G₀ : Type u_1} {M₀ : Type u_2} [Monoid G₀] [AddMonoid M₀] [h : DistribMulAction G₀ M₀] :
DistribMulAction G₀ᵒᵈ M₀
source
🔸 coverage
@[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₀ᵒᵈ
source
🔸 coverage
@[implicit_reducible]
instance OrderDual.instMulActionWithZero {G₀ : Type u_1} {M₀ : Type u_2} [MonoidWithZero G₀] [AddMonoid M₀] [h : MulActionWithZero G₀ M₀] :
MulActionWithZero G₀ᵒᵈ M₀
source
🔸 coverage
@[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₀ᵒᵈ
source
🔸 coverage
@[implicit_reducible]
instance Lex.instSMulWithZero {G₀ : Type u_1} {M₀ : Type u_2} [Zero G₀] [Zero M₀] [SMulWithZero G₀ M₀] :
SMulWithZero (Lex G₀) M₀
source
🔸 coverage
@[implicit_reducible]
instance Lex.instSMulWithZero' {G₀ : Type u_1} {M₀ : Type u_2} [Zero G₀] [Zero M₀] [SMulWithZero G₀ M₀] :
SMulWithZero G₀ (Lex M₀)
source
🔸 coverage
@[implicit_reducible]
instance Lex.instDistribSMul {G₀ : Type u_1} {M₀ : Type u_2} [AddZeroClass M₀] [DistribSMul G₀ M₀] :
DistribSMul (Lex G₀) M₀
source
🔸 coverage
@[implicit_reducible]
instance Lex.instDistribSMul' {G₀ : Type u_1} {M₀ : Type u_2} [AddZeroClass M₀] [DistribSMul G₀ M₀] :
DistribSMul G₀ (Lex M₀)
source
🔸 coverage
@[implicit_reducible]
instance Lex.instDistribMulAction {G₀ : Type u_1} {M₀ : Type u_2} [Monoid G₀] [AddMonoid M₀] [DistribMulAction G₀ M₀] :
DistribMulAction (Lex G₀) M₀
source
🔸 coverage
@[implicit_reducible]
instance Lex.instDistribMulAction' {G₀ : Type u_1} {M₀ : Type u_2} [Monoid G₀] [AddMonoid M₀] [DistribMulAction G₀ M₀] :
DistribMulAction G₀ (Lex M₀)
source
🔸 coverage
@[implicit_reducible]
instance Lex.instMulActionWithZero {G₀ : Type u_1} {M₀ : Type u_2} [MonoidWithZero G₀] [AddMonoid M₀] [MulActionWithZero G₀ M₀] :
MulActionWithZero (Lex G₀) M₀
source
🔸 coverage
@[implicit_reducible]
instance Lex.instMulActionWithZero' {G₀ : Type u_1} {M₀ : Type u_2} [MonoidWithZero G₀] [AddMonoid M₀] [MulActionWithZero G₀ M₀] :
MulActionWithZero G₀ (Lex M₀)