Theorems · Inductive type · group theory
InvolutiveNeg
Type u_2 → Type u_2
Auxiliary typeclass for types with an involutive Neg.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 151 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by177
Results whose statement or proof uses this declaration.
- neg_negstatement and proof · cited by 960
- neg_injstatement and proof · cited by 85
- neg_eq_iff_eq_negstatement and proof · cited by 60
- Equiv.negstatement and proof · cited by 53
- Set.image_neg_eq_negstatement and proof · cited by 52
- neg_mem_iffstatement and proof · cited by 42
- neg_injectivestatement and proof · cited by 35
- Equiv.neg_applystatement and proof · cited by 34
- RootPairing.indexNegstatement · cited by 33
- Homeomorph.negstatement and proof · cited by 24
- Set.neg_singletonstatement and proof · cited by 14
- Finset.card_negstatement and proof · cited by 12