Mathlib Map

Theorems · Inductive type · general algebraic systems

IsVAddApply

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

IsVAddApply M F α β states for all f : F, n : M and x : α, (n +ᵥ f) x = n +ᵥ f x.

Defined in
Mathlib.Data.FunLike.IsApply
Cited by
3 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
FunLikeVAddVAdd
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsVAddApply.vadd_apply · cited by 1IsVAddApply.vadd_applyvadd_apply · cited by 1vadd_applyFunLike.addAction · cited by 0FunLike.addActionFunLike.coe_vadd · cited by 0FunLike.coe_vaddIsVAddApply.casesOn · cited by 0IsVAddApply.casesOnIsVAddApply.recOn · cited by 0IsVAddApply.recOnFunLike · cited by 2560FunLikeVAdd · cited by 616VAddIsVAddApplyCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • FunLikestatement · cited by 2,560
  • VAddstatement · cited by 616

Cited by6

Results whose statement or proof uses this declaration.