OAI/GroupTheory/PolycyclicRecognition/Finiteness/IntegerInducedCochains.lean
5 declarations, 0 contain sorry, 0 declared as axioms
Integer coordinates on the induced resolution and its cohomology
- def
OAI.PolycyclicRecognition.integerInducedCochainsIsoline 23 - theorem
OAI.PolycyclicRecognition.integerInducedCochainsIso_applyline 31 - theorem
OAI.PolycyclicRecognition.integerInducedCochainsIso_translationline 37 - def
OAI.PolycyclicRecognition.integerInducedCohomologyIsoline 56 - theorem
OAI.PolycyclicRecognition.integerInducedCohomologyIso_translationline 64