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.
theorem FunLike.isScalarTower {M : Type u_1} {M' : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [SMul M β] [SMul M' β] [SMul M F] [SMul M' F] [IsSMulApply M F] [IsSMulApply M' F] [SMul M M'] [IsScalarTower M M' β] :
IsScalarTower M M' F
theorem FunLike.smulCommClass {M : Type u_1} {M' : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [SMul M β] [SMul M' β] [SMul M F] [SMul M' F] [IsSMulApply M F] [IsSMulApply M' F] [SMulCommClass M M' β] :
SMulCommClass M M' F
theorem FunLike.vaddCommClass {M : Type u_1} {M' : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [VAdd M β] [VAdd M' β] [VAdd M F] [VAdd M' F] [IsVAddApply M F] [IsVAddApply M' F] [VAddCommClass M M' β] :
VAddCommClass M M' F
theorem FunLike.isCentralScalar {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [SMul M F] [SMul Mᵐᵒᵖ F] [SMul M β] [SMul Mᵐᵒᵖ β] [IsCentralScalar M β] [IsSMulApply M F] [IsSMulApply Mᵐᵒᵖ F] :
IsCentralScalar M F
@[reducible, inline]
abbrev FunLike.mulAction {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [SMul M F] [Monoid M] [MulAction M β] [IsSMulApply M F] :
MulAction M F
A FunLike type with scalar multiplication that satisfies (m • f) x = m • f x
is a MulAction if β is a MulAction.
Equations
Instances For
@[reducible, inline]
abbrev FunLike.addAction {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [VAdd M F] [AddMonoid M] [AddAction M β] [IsVAddApply M F] :
AddAction M F
A FunLike type with scalar multiplication that satisfies (m • f) x = m • f x
is an AddAction if β is an AddAction.