OAI/GroupTheory/FiniteIndex/Powers.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite generation and power subgroups of abelian groups.

  1. lemma OAI.FiniteIndexRealization.elementary_finite_of_fg_bounded_exponent line 12
  2. lemma OAI.FiniteIndexRealization.elementary_finiteIndex_powers line 29