Theorems · Theorem · general algebraic systems

smul_apply

∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x

Alias of IsSMulApply.smul_apply.

Defined in

Mathlib.Data.FunLike.IsApply

Cited by

229 results in Mathlib

Foundations

Depth 5 from the axioms, rests on 11 definitions · uses no axioms

Assumes

IsSMulApply