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