Theorems · Theorem · general algebraic systems

add_apply

∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x

Alias of IsAddApply.add_apply.

Defined in

Mathlib.Data.FunLike.IsApply

Cited by

154 results in Mathlib

Foundations

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

Assumes

IsAddApply