Theorems · Theorem · group theory
AddSubgroup.FiniteIndex.index_ne_zero
∀ {G : Type u_3} {inst : AddGroup G} {H : AddSubgroup G} [self : H.FiniteIndex], H.index ≠ 0The additive subgroup has finite index;
recall that AddSubgroup.index returns 0 when the index is infinite.
- Defined in
- Mathlib.GroupTheory.Index
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddSubgroup.FiniteIndex
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement and proof · cited by 3,232
- AddSubgroup.indexstatement · cited by 104
- AddSubgroup.FiniteIndexstatement and proof · cited by 66
Cited by11
Results whose statement or proof uses this declaration.
- AddSubgroup.finiteIndex_iffproof · cited by 4
- AddSubgroup.fintypeQuotientOfFiniteIndexproof · cited by 3
- AddSubgroup.leftCoset_cover_filter_FiniteIndex_auxproof · cited by 3
- Ideal.absNorm_ne_zero_iffproof · cited by 2
- AddSubgroup.finiteIndex_iInfproof · cited by 2
- AddSubgroup.finiteIndex_of_leproof · cited by 1
- AddSubgroup.finite_iff_finite_and_finiteIndexproof · cited by 1
- AddSubgroup.finrank_eq_of_finiteIndexproof · cited by 1
- AddSubgroup.index_antitoneproof · cited by 1
- AddSubgroup.index_rangeproof · cited by 1
- AddSubgroup.index_strictAntiproof · cited by 0