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] [Zero α] [IsZeroApply F α α] [IsOneApplyEqSelf F α] [IsMulApplyEqComp 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.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 ⋯ ⋯ ⋯