OAI/GroupTheory/PolycyclicRecognition/Analysis/NoetherianIntegralTorsion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform exponent for integral torsion in a noetherian module

The coefficient ring may be a group ring. Only its noetherian module condition is used to choose finitely many generators of the integral torsion submodule.

  1. theorem OAI.PolycyclicRecognition.noetherian_integral_torsion_exponent line 17