OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianNormalLargePrimeRank.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite prime reductions outside a fixed finite set

The same integer group generators bound the necessary exterior degree for all coefficient fields. When the characteristic exceeds that degree, the factorial comparison in actual homology is invertible.

  1. theorem OAI.PolycyclicRecognition.abelian_normal_large_prime_scalar_rank line 23
  2. theorem OAI.PolycyclicRecognition.abelian_normal_large_prime_reduction_finite line 54