OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalCompleteIdentity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Rational vanishing gives an integral annihilator of the complete identity

This is the coefficient step in the torsion endgame. Rational vanishing remains an explicit intermediate premise until the hierarchical argument supplies it.

  1. instance OAI.PolycyclicRecognition.groupCohomology_integral_additive line 18
  2. theorem OAI.PolycyclicRecognition.completedCohomologyMap_scalar_identity line 26
  3. theorem OAI.PolycyclicRecognition.TypeFPInfinity.completedIdentity_factorial_annihilator line 42
  4. theorem OAI.PolycyclicRecognition.TypeFPInfinity.boundedFiniteSubgroupOrders_of_rational_vanishing line 55
  5. theorem OAI.PolycyclicRecognition.TypeFPInfinity.boundedFiniteSubgroupOrders_of_rational_projectiveDimension line 63