Theorems · Theorem · group theory
Subgroup.mul_mem
∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x y : G}, x ∈ H → y ∈ H → x * y ∈ HA subgroup is closed under multiplication.
- Defined in
- Mathlib.Algebra.Group.Subgroup.Defs
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- Subgroupstatement and proof · cited by 3,593
- MulMemClass.mul_memproof · cited by 173
Cited by30
Results whose statement or proof uses this declaration.
- Subgroup.mul_mem_supproof · cited by 6
- Subgroup.commutator_le_rightproof · cited by 4
- MulAction.IwasawaStructure.commutator_leproof · cited by 4
- Subgroup.isOpen_of_mem_nhdsproof · cited by 3
- MonoidWithZeroHom.mem_valueGroup_iff_of_commproof · cited by 3
- Subgroup.conj_smul_le_of_leproof · cited by 2
- IsPGroup.exists_le_sylowproof · cited by 2
- DoubleCoset.mem_doubleCoset_of_not_disjointproof · cited by 1
- Group.fg_of_descentproof · cited by 1
- QuotientGroup.strictMono_comap_prod_imageproof · cited by 1
- Equiv.Perm.closure_cycle_adjacent_swapproof · cited by 1
- GrpCat.SurjectiveOfEpiAuxs.agreeproof · cited by 1