OAI/GroupTheory/PolycyclicRecognition/Algebra/CentralLayerTensor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Tensor generators of a central commutator layer

  1. def OAI.PolycyclicRecognition.centralLayerSubmodule line 16
  2. theorem OAI.PolycyclicRecognition.centralLayerPairing_mem line 19
  3. def OAI.PolycyclicRecognition.centralLayerTensor line 25
  4. theorem OAI.PolycyclicRecognition.centralLayerTensor_mem line 30
  5. def OAI.PolycyclicRecognition.centralLayerTensorSurjection line 37
  6. theorem OAI.PolycyclicRecognition.centralLayerTensor_range line 41
  7. theorem OAI.PolycyclicRecognition.centralLayerTensor_surjective line 63
  8. theorem OAI.PolycyclicRecognition.centralLayer_scalar_finite line 73
  9. def OAI.PolycyclicRecognition.centralLayerAddEquiv line 85
  10. theorem OAI.PolycyclicRecognition.central_commutator_scalar_finite line 94