Structures · Algebra
InvolutiveNeg
Auxiliary typeclass for types with an involutive Neg.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds neg_neg
Extends1
Extended by2
Concrete types that are instances23
- SeparationQuotient
- Filter.Germ
- Matrix
- EReal
- DomAddAct
- LieModule.Weight
- LinearPMap
- WeierstrassCurve.Affine.Point
- MeasureTheory.JordanDecomposition
- RayVector
- ConjRootClass
- Module.Ray
- Prod
- OrderDual
- Set.Elem
- MulOpposite
- Fin
- Lex
- AddOpposite
- Colex
- Additive
- WithZero
- Set
How is a type an instance?
Loading the hierarchy index…
Assumed by147
- neg_neg
- neg_inj
- neg_eq_iff_eq_neg
- Equiv.neg
- Set.image_neg_eq_neg
- neg_mem_iff
- neg_injective
- Equiv.neg_apply
- Homeomorph.neg
- Set.neg_singleton
- Function.Antiperiodic.sub_eq
- Finset.card_neg
- neg_surjective
- neg_involutive
- Finset.mem_neg'
- Set.neg_mem_neg
- Function.Antiperiodic.periodic_two_mul
- IsCompact.neg
- MeasurableEquiv.neg
- Set.neg_subset
- Set.neg_subset_neg
- IsAddIndecomposable.mem_or_neg_mem_closure_baseOf
- Set.nonempty_neg
- Finset.coe_neg
- IsOpen.neg
- Function.Periodic.sub_antiperiod_eq
- Function.Antiperiodic.neg
- Set.Nonempty.neg
- neg_coe_set
- MeasureTheory.Measure.neg_neg
- Function.Antiperiodic.periodic
- Set.finite_neg
- AddSubmonoid.apply_ne_zero_of_mem_or_neg_mem_closure
- Function.Odd.sum_eq_zero
- MeasureTheory.Measure.neg_apply
- Function.Odd.finsetSum_eq_zero
- Finset.neg_univ
- tsum_comp_neg
- Function.Antiperiodic.even_nsmul_periodic
- MeasurableEquiv.neg_apply
- Function.Antiperiodic.even_zsmul_periodic
- neg_closure
- MeasureTheory.lintegral_neg_eq_self
- Finset.neg_filter
- IsClosed.neg
- IsAddIndecomposable.pairwise_sub_notMem_range'
- Function.Antiperiodic.int_even_mul_periodic
- IsAddIndecomposable.pairwise_baseOf_sub_notMem
- Set.ncard_neg
- Set.image_neg_of_apply_neg_eq