Theorems · Definition · group theory

FunLike.involutiveNeg

{F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] → [inst_1 : Neg F] → [inst_2 : InvolutiveNeg β] → [IsNegApply F α β] → InvolutiveNeg F

A FunLike type with negation that satisfies (- f) x = - (f x) is an involutive negation if β is an involutive negation.

Defined in: Mathlib.Data.FunLike.Group
Cited by: 0 results in Mathlib
Foundations: Depth 8 from the axioms · uses propext, Quot.sound
Assumes: FunLike Neg InvolutiveNeg IsNegApply

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

DFunLike.coeproof · cited by 62,936
FunLikestatement and proof · cited by 2,560
InvolutiveNegstatement and proof · cited by 151
IsNegApplystatement and proof · cited by 21
Function.Injective.involutiveNegproof · cited by 0

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.