Theorems · Theorem · group theory
mul_mem_cancel_right
∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [SubgroupClass S G] {x y : G},
x ∈ H → (y * x ∈ H ↔ y ∈ H)- Defined in
- Mathlib.Algebra.Group.Subgroup.Defs
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
- Assumes
- GroupSetLikeSubgroupClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- SetLikestatement and proof · cited by 1,084
- MulMemClass.mul_memproof · cited by 173
- mul_inv_cancel_rightproof · cited by 53
- InvMemClass.inv_memproof · cited by 52
- SubgroupClassstatement and proof · cited by 34
Cited by11
Results whose statement or proof uses this declaration.
- Subgroup.mul_mem_cancel_rightproof · cited by 7
- Subgroup.mul_mem_iff_of_index_twoproof · cited by 3
- Subgroup.le_normalizer_iff_commutator_le_rightproof · cited by 1
- HNNExtension.ReducedWord.exists_normalWord_prod_eqproof · cited by 1
- Subgroup.normalizer_commutator_ge_leftproof · cited by 1
- rightCoset_mem_rightCosetproof · cited by 1
- Subgroup.IsComplement.equiv_fst_eq_iff_leftCosetEquivalenceproof · cited by 1
- Subgroup.subgroup_mul_singletonproof · cited by 1
- SubgroupClass.subset_unionproof · cited by 0
- MulAction.IsBlock.of_orbitproof · cited by 0
- MulAction.stabilizer_orbit_eqproof · cited by 0