OAI/GroupTheory/PolycyclicRecognition/Geometry/RotationExponentialProduct.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Global exponential factor coordinates and cancellation

  1. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationExponentialProduct line 22
  2. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationExponentialProduct_surjective line 26
  3. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotationExponentialProduct_eq_one line 31