OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianNormalFiniteRank.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite rational rank of every abelian kernel in the abelian-quotient case

Actual FP-infinity supplies all higher homology modules. Their natural maps to exterior powers, followed by the free-orbit obstruction, give finite rank without a cyclic quotient or a rank assumption on the kernel.

  1. theorem OAI.PolycyclicRecognition.abelian_normal_kernel_finite_scalar_rank line 20
  2. theorem OAI.PolycyclicRecognition.abelian_normal_kernel_finite_rank line 29