OAI/GroupTheory/PolycyclicRecognition/Algebra/UpperCentralLayerMap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Equivariant rational maps from the actual upper central series

  1. theorem OAI.PolycyclicRecognition.mem_ambientUpperCentralSeries_iff line 15
  2. def OAI.PolycyclicRecognition.ambientUpperCentralToF line 24
  3. def OAI.PolycyclicRecognition.upperCentralLayerMap line 27
  4. theorem OAI.PolycyclicRecognition.upperCentralLayerMap_equivariant line 37
  5. def OAI.PolycyclicRecognition.rationalUpperCentralMap line 49
  6. theorem OAI.PolycyclicRecognition.rationalUpperCentralMap_equivariant line 55
  7. theorem OAI.PolycyclicRecognition.rationalUpperCentralMap_kernel line 67