Theorems · Inductive type · general algebraic systems

IsMulApply

(F : Type u_1) → (α : outParam (Type u_2)) → (β : outParam (Type u_3)) → [FunLike F α β] → [Mul β] → [Mul F] → Prop

IsMulApply F α β states for all f g : F and x : α, (f * g) x = f x * g x.

Defined in

Mathlib.Data.FunLike.IsApply

Cited by

18 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

FunLikeMulMul