Structures · Algebra
NegMemClass
NegMemClass S G states S is a type of subsets s ⊆ G closed under negation.
- Defined in
- Mathlib.Algebra.Group.Subgroup.Defs
- Shape
- 2 explicit arguments · adds neg_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by16
- NegMemClass.neg_mem
- neg_mem_iff
- neg_coe_set
- HomogeneousLocalization.val_neg
- abs_mem_iff
- HomogeneousLocalization.mk_neg
- Set.injOn_iff_map_eq_zero
- RestrictedProduct.neg_apply
- NegMemClass.neg
- RestrictedProduct.instNegCoeOfNegMemClass
- HomogeneousLocalization.NumDenSameDeg.den_neg
- RestrictedProduct.instContinuousNegCoe
- HomogeneousLocalization.NumDenSameDeg.instNeg
- HomogeneousLocalization.NumDenSameDeg.num_neg
- HomogeneousLocalization.instNeg
- HomogeneousLocalization.NumDenSameDeg.deg_neg
Ancestors0
No ancestors.