Theorems · Theorem · group theory
neg_mem_iff
∀ {S : Type u_3} {G : Type u_4} [inst : InvolutiveNeg G] {x : SetLike S G} [NegMemClass S G] {H : S} {x_1 : G},
-x_1 ∈ H ↔ x_1 ∈ H- Defined in
- Mathlib.Algebra.Group.Subgroup.Defs
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- InvolutiveNegNegMemClass
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.
- SetLikestatement and proof · cited by 1,084
- neg_negproof · cited by 960
- InvolutiveNegstatement and proof · cited by 151
- NegMemClass.neg_memproof · cited by 63
- NegMemClassstatement and proof · cited by 11
Cited by42
Results whose statement or proof uses this declaration.
- Submodule.neg_mem_iffproof · cited by 11
- AddSubgroup.zmultiples_negproof · cited by 6
- AddSubgroup.index_eq_two_iffproof · cited by 5
- LieSubalgebra.mem_normalizer_iffproof · cited by 5
- AddSubgroup.neg_mem_iffproof · cited by 5
- Submodule.quotientRel_defproof · cited by 4
- EuclideanGeometry.coe_orthogonalProjection_eq_iff_memproof · cited by 4
- LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_topproof · cited by 4
- neg_coe_setproof · cited by 3
- vadd_coe_setproof · cited by 3
- QuotientAddGroup.preimage_image_mkproof · cited by 2
- AddSubgroup.index_eq_two_iff'proof · cited by 2