Theorems · Inductive type · general algebraic systems

IsAddApply

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

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

Defined in

Mathlib.Data.FunLike.IsApply

Cited by

75 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

FunLikeAddAdd