Subgroup.FiniteIndex

Extends nothing: this is a root of the hierarchy.

Nothing extends this class yet.

• Matrix.SpecialLinearGroup
• Subtype
• Prod

Loading the hierarchy index…

• Rep.indCoindIso
• Subgroup.FiniteIndex.index_ne_zero
• MonoidHom.transferSylow
• Subgroup.fintypeQuotientOfFiniteIndex
• Sylow.not_dvd_index
• Subgroup.leftTransversals.diff
• MonoidHom.transfer
• Rep.coindToInd
• Rep.indCoindNatIso
• Subgroup.transferFocal
• Rep.coindResAdjunction
• Rep.resIndAdjunction
• Subgroup.leftTransversals.diff_mul_diff
• MonoidHom.transferCenterPow
• Subgroup.QuotientDiff
• Subgroup.finiteIndex_of_le
• MonoidHom.ker_transferSylow_isComplement'
• Subgroup.smul_diff'
• MonoidHom.transferSylow_domRestrict_eq_pow
• MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot
• Subgroup.index_antitone
• FiniteIndexNormalSubgroup.ofSubgroup
• Subgroup.leftTransversals.diff_inv
• Subgroup.leftTransversals.diff_self
• Subgroup.isOpen_of_isClosed_of_finiteIndex
• Subgroup.transferFocal_eq_pow
• Rep.coindToInd_apply
• MonoidHom.transfer_eq_pow
• MonoidHom.transferSylow_eq_pow
• Subgroup.ker_restrict_transferFocal_eq_focalSubgroupOf
• Subgroup.index_range
• Subgroup.exists_smul_eq
• Rep.indCoindIso_hom_hom_toLinearMap
• Sylow.finite_of_finiteIndex
• Subgroup.focalSubgroupOf.pow_index_surjective
• Rep.coindToInd_of_support_subset_orbit
• Subgroup.ker_transferFocal_inf_eq_focalSubgroup
• Rep.coindToInd_indToCoind
• Subgroup.IsComplement.finite_left
• MonoidHom.transfer_def
• IsPGroup.index
• Subgroup.exists_leftTransversal_of_FiniteIndex
• ModularGroup.exists_bound_of_subgroup_invariant_of_isBigO
• Subgroup.leftTransversals.smul_diff_smul
• Subgroup.IsComplement.encard_left
• Subgroup.exists_finset_card_le_mul
• Subgroup.discreteTopology_iff_of_finiteIndex
• Subgroup.IsComplement.finite_right
• Subgroup.eq_one_of_smul_eq_one
• Rep.indToCoind_coindToInd

No ancestors.