Structures · Algebra
SubgroupClass
SubgroupClass S G states S is a type of subsets s ⊆ G that are subgroups of G.
- Defined in
- Mathlib.Algebra.Group.Subgroup.Defs
- Shape
- 2 explicit arguments
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- OpenSubgroup
- OpenNormalSubgroup
- FiniteIndexNormalSubgroup
- Sylow
- ClosedSubgroup
- Subgroup
How is a type an instance?
Loading the hierarchy index…
Assumed by54
- mul_mem_cancel_right
- mul_mem_cancel_left
- div_mem
- zpow_mem
- SubgroupClass.inclusion
- SubgroupClass.subtype
- smul_coe_set
- op_smul_coe_set
- exists_inv_mem_iff_exists_mem
- Subgroup.ofClass
- IsApproximateSubgroup.subgroup
- div_mem_comm_iff
- RestrictedProduct.instLocallyCompactSpaceCoeCofiniteOfSubgroupClassOfIsTopologicalGroupOfCompactSpaceSubtypeMem
- SubgroupClass.toGroup
- SubgroupClass.coe_pow
- SubgroupClass.seminormedCommGroup
- SubgroupClass.toCommGroup
- SubgroupClass.coe_inclusion
- RestrictedProduct.instGroupCoeOfSubgroupClass
- SubgroupClass.inclusion_mk
- RestrictedProduct.div_apply
- SubgroupClass.coe_subtype
- SubgroupClass.subtype_injective
- InvMemClass.coe_inv
- SubgroupClass.coe_zpow
- SubgroupClass.coe_norm
- RestrictedProduct.instCommGroupCoeOfSubgroupClass
- SubgroupClass.inclusion_right
- Subgroup.coe_ofClass
- RestrictedProduct.isTopologicalGroup
- RestrictedProduct.instZPow
- MulAction.isBlock_subgroup'
- RestrictedProduct.locallyCompactSpace_of_group
- SubgroupClass.toInvMemClass
- RestrictedProduct.instDivCoeOfSubgroupClass
- SubgroupClass.instZPow
- SubgroupClass.normedCommGroup
- SubgroupClass.inclusion_inclusion
- SubgroupClass.coe_div
- RestrictedProduct.mulSingle_div
- SubgroupClass.subtype_comp_inclusion
- RestrictedProduct.mulSingle_inv
- coe_div_coe
- RestrictedProduct.instIsTopologicalGroupCoePrincipal
- MulAction.isBlock_subgroup
- SubgroupClass.inclusion_self
- RestrictedProduct.mulSingle_zpow
- SubgroupClass.div
- SubgroupClass.toSubmonoidClass
- SubgroupClass.subtype_apply