OAI/GroupTheory/PolycyclicRecognition/Algebra/ResidualLowerCentralLayers.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Group commutators on the joint-fixed lower-central layers

  1. abbrev OAI.PolycyclicRecognition.JointFixedReductionData.residualKernelLayer line 24
  2. def OAI.PolycyclicRecognition.JointFixedReductionData.residualLayer line 27
  3. instance OAI.PolycyclicRecognition.JointFixedReductionData.residualLayer_normal line 30
  4. def OAI.PolycyclicRecognition.JointFixedReductionData.residualLayerEquiv line 41
  5. def OAI.PolycyclicRecognition.JointFixedReductionData.residualLayerProjection line 44
  6. theorem OAI.PolycyclicRecognition.JointFixedReductionData.residualLayerProjection_equiv line 49
  7. theorem OAI.PolycyclicRecognition.JointFixedReductionData.residualLayerProjection_kernel_le line 56
  8. theorem OAI.PolycyclicRecognition.JointFixedReductionData.residualLayerProjection_equivariant line 68
  9. theorem OAI.PolycyclicRecognition.JointFixedReductionData.residualLayer_commutator_bound line 93