OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalAbelianTorsion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Rationalization detects torsion in abelian groups

  1. theorem OAI.PolycyclicRecognition.rational_module_isZero_of_surjective line 14
  2. theorem OAI.PolycyclicRecognition.rationalAbelianMap_eq_zero_iff_isOfFinOrder line 23
  3. theorem OAI.PolycyclicRecognition.rationalAbelianSpace_isZero_iff_torsion line 40