SMul instances for FunLike types

In this file we define various instances related to scalar multiplications for FunLike types.

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

@[reducible, inline]

abbrev FunLike.distribSMul {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [AddZeroClass β] [AddZeroClass F] [DistribSMul M β] [SMul M F] [IsZeroApply F] [IsAddApply F] [IsSMulApply M F] : DistribSMul M F

A FunLike type with scalar multiplication that satisfies (m • f) x = m • f x and 0 x = 0, (f + g) x = f x + g x is a DistribSMul if β is a DistribSMul.

Equations

• FunLike.distribSMul = Function.Injective.distribSMul (FunLike.coeAddMonoidHom F α β) ⋯ ⋯

@[reducible, inline]

abbrev FunLike.distribMulAction {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [Monoid M] [AddMonoid β] [AddMonoid F] [DistribMulAction M β] [SMul M F] [IsZeroApply F] [IsAddApply F] [IsSMulApply M F] : DistribMulAction M F

A FunLike type with scalar multiplication that satisfies (m • f) x = m • f x, 0 x = 0, (f + g) x = f x + g x is a DistribMulAction if β is a DistribMulAction.

Equations

• FunLike.distribMulAction = Function.Injective.distribMulAction (FunLike.coeAddMonoidHom F α β) ⋯ ⋯