Structures · Algebra
AddSubgroup.FiniteIndex
Typeclass for finite index subgroups.
- Defined in
- Mathlib.GroupTheory.Index
- Shape
- One type argument · adds index_ne_zero
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Subtype
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by33
- AddSubgroup.FiniteIndex.index_ne_zero
- AddSubgroup.leftTransversals.diff
- AddSubgroup.isOpen_of_isClosed_of_finiteIndex
- AddSubgroup.leftTransversals.diff_add_diff
- AddSubgroup.fintypeQuotientOfFiniteIndex
- FiniteIndexNormalAddSubgroup.ofAddSubgroup
- AddMonoidHom.transfer
- AddSubgroup.index_antitone
- AddSubgroup.leftTransversals.vadd_diff_vadd
- AddSubgroup.finrank_eq_of_finiteIndex
- AddSubgroup.leftTransversals.diff_self
- AddSubgroup.discreteTopology_iff_of_finiteIndex
- AddSubgroup.index_range
- AddSubgroup.isFiniteRelIndex_of_finiteIndex
- AddSubgroup.IsComplement.finite_left
- AddSubgroup.IsComplement.finite_right
- AddSubgroup.finiteIndex_of_le
- AddSubgroup.IsComplement.encard_left
- AddSubgroup.exists_leftTransversal_of_FiniteIndex
- FiniteIndexNormalAddSubgroup.toAddSubgroup_ofAddSubgroup
- AddSubgroup.leftTransversals.diff_neg
- AddSubgroup.transferFocal
- AddSubgroup.instFiniteIndex_addSubgroupOf
- AddSubgroup.instFiniteIndexMin
- AddSubgroup.exists_finset_card_le_add
- AddSubgroup.finiteIndex_normalCore
- AddSubgroup.IsComplement.encard_right
- MeasureTheory.AddSubgroup.index_mul_measure
- AddSubgroup.fg_of_index_ne_zero
- AddSubgroup.index_strictAnti
- AddSubgroup.finite_quotient_of_finiteIndex
- AddMonoidHom.transfer_def
- AddSubgroup.instFiniteIndexSumSum
Ancestors0
No ancestors.