Theorems · Theorem · group theory
AddSubgroup.mem_inf
∀ {G : Type u_1} [inst : AddGroup G] {p p' : AddSubgroup G} {x : G}, x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'- Defined in
- Mathlib.Algebra.Group.Subgroup.Lattice
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext
- Assumes
- AddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement and proof · cited by 3,232
Cited by8
Results whose statement or proof uses this declaration.
- AddAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂proof · cited by 3
- AddSubgroup.addSubgroupOf_injproof · cited by 3
- AddSubgroup.normalizer_inf_normalizer_le_normalizer_supproof · cited by 2
- AddSubgroup.disjoint_defproof · cited by 1
- AddSubgroup.exists_nsmul_mem_of_relIndex_ne_zeroproof · cited by 0
- AddSubgroup.nsmul_mem_of_relIndex_ne_zero_of_dvdproof · cited by 0
- SubAddAction.mem_fixingAddSubgroup_union_iffproof · cited by 0
- AddAction.orbitRel_addSubgroupOfproof · cited by 0