OAI/GroupTheory/PolycyclicRecognition/Geometry/RotationFactorAction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The Cartan action on the nilpotent factor of the rotational graph

  1. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationFactorAction line 23
  2. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationFactorAction_conjugation line 28
  3. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationFactorAction_exponential line 34