Theorems · Definition · general algebraic systems

IsNegApply.recOn

{F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Neg β] →
          [inst_2 : Neg F] →
            {motive : IsNegApply F α β → Sort u} →
              (t : IsNegApply F α β) → ((neg_apply : ∀ (f : F) (x : α), (-f) x = -f x) → motive ⋯) → motive t

Defined in: Mathlib.Data.FunLike.IsApply
Cited by: 0 results in Mathlib
Foundations: Depth 6 from the axioms · uses no axioms
Assumes: FunLike Neg Neg

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites3

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

DFunLike.coestatement and proof · cited by 62,936
FunLikestatement and proof · cited by 2,560
IsNegApplystatement and proof · cited by 21

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.