Group with zero instances for FunLike types

In this file we define various instances related to GroupWithZero for FunLike types. There are two different variants: either the multiplication is given by composition or it is pointwise multiplication.

Note that currently, these are not registered as instances, but only abbrevs to avoid long typeclass searches.

@[reducible, inline]

abbrev FunLike.compMonoidWithZero {F : Type u_1} {α : Type u_2} [FunLike F α α] [Zero F] [One F] [Mul F] [NPow F] [Zero α] [IsZeroApply F] [IsOneApplyEqSelf F] [IsMulApplyEqComp F] [IsNPowApplyEqIterate F] [ZeroHomClass F α α] : MonoidWithZero F

A FunLike type with (f * g) x = f (g x) is a MonoidWithZero

Equations

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

@[reducible, inline]

abbrev FunLike.smulWithZero {F : Type u_1} {α : Type u_2} {β : Type u_3} {R : Type u_4} [FunLike F α β] [Zero β] [Zero F] [IsZeroApply F] [Zero R] [SMulWithZero R β] [SMul R F] [IsSMulApply R F] : SMulWithZero R F

A FunLike type with (r • f) x = r • f x is a SMulWithZero if β is a SMulWithZero.

Equations

• FunLike.smulWithZero = Function.Injective.smulWithZero { toFun := DFunLike.coe, map_zero' := ⋯ } ⋯ ⋯

@[reducible, inline]

abbrev FunLike.mulActionWithZero {F : Type u_1} {α : Type u_2} {β : Type u_3} {R : Type u_4} [FunLike F α β] [Zero β] [Zero F] [IsZeroApply F] [MonoidWithZero R] [MulActionWithZero R β] [SMul R F] [IsSMulApply R F] : MulActionWithZero R F

A FunLike type with (r • f) x = r • f x is a MulActionWithZero if β is a MulActionWithZero.

Equations

• FunLike.mulActionWithZero = Function.Injective.mulActionWithZero { toFun := DFunLike.coe, map_zero' := ⋯ } ⋯ ⋯

@[reducible, inline]

abbrev FunLike.mulZeroClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [Mul F] [MulZeroClass β] [IsZeroApply F] [IsMulApply F] : MulZeroClass F

A FunLike type with (f * g) x = f x * g x is a MulZeroClass if β is a MulZeroClass.

Equations

• FunLike.mulZeroClass = Function.Injective.mulZeroClass DFunLike.coe ⋯ ⋯ ⋯

@[reducible, inline]

abbrev FunLike.mulZeroOneClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [One F] [Mul F] [MulZeroOneClass β] [IsZeroApply F] [IsMulApply F] [IsOneApply F] : MulZeroOneClass F

A FunLike type with (f * g) x = f x * g x is a MulZeroOneClass if β is a MulZeroOneClass.

Equations

• FunLike.mulZeroOneClass = Function.Injective.mulZeroOneClass DFunLike.coe ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev FunLike.monoidWithZero {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [One F] [Mul F] [Pow F ℕ] [MonoidWithZero β] [IsZeroApply F] [IsMulApply F] [IsOneApply F] [IsPowApply ℕ F] : MonoidWithZero F

A FunLike type with (f * g) x = f x * g x is a MonoidWithZero if β is a MonoidWithZero.

Equations

• FunLike.monoidWithZero = Function.Injective.monoidWithZero DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev FunLike.commMonoidWithZero {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [One F] [Mul F] [Pow F ℕ] [CommMonoidWithZero β] [IsZeroApply F] [IsMulApply F] [IsOneApply F] [IsPowApply ℕ F] : CommMonoidWithZero F

A FunLike type with (f * g) x = f x * g x is a CommMonoidWithZero if β is a CommMonoidWithZero.

Equations

• FunLike.commMonoidWithZero = Function.Injective.commMonoidWithZero DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev FunLike.semigroupWithZero {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [Mul F] [SemigroupWithZero β] [IsZeroApply F] [IsMulApply F] : SemigroupWithZero F

A FunLike type with (f * g) x = f x * g x is a SemigroupWithZero if β is a SemigroupWithZero.

Equations

• FunLike.semigroupWithZero = Function.Injective.semigroupWithZero DFunLike.coe ⋯ ⋯ ⋯