Theorems · Theorem · group theory

AddSubgroup.finrank_eq_of_finiteIndex

∀ {M : Type u_1} [inst : AddCommGroup M] [Module.Finite ℤ M] [Module.IsTorsionFree ℤ M] (A : AddSubgroup M)
  [A.FiniteIndex], Module.finrank ℤ ↥A = Module.finrank ℤ M

If A is a subgroup of finite index of an additive group M that is finitely generated and torsion-free as a ℤ-module, then A and M have the same rank.

Defined in

Mathlib.GroupTheory.IndexNSmul

Cited by

1 results in Mathlib

Foundations

Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupModule.FiniteModule.IsTorsionFreeAddSubgroup.FiniteIndex