OAI/GroupTheory/PolycyclicRecognition/Finiteness/TensorProjectiveTower.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The projective tower tensored with the coefficient algebra

For a coefficient projective over the integers, tensoring the normalized integral tower gives an actual projective tower, based at that coefficient.

  1. def OAI.PolycyclicRecognition.tensorNormalizedProjectiveTower line 20
  2. def OAI.PolycyclicRecognition.tensorNormalizedTowerBaseIso line 33
  3. def OAI.PolycyclicRecognition.tensorNormalizedTowerCompletion line 36