OAI/GroupTheory/PolycyclicRecognition/Geometry/IndividualRotationDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The compact rotation has its prescribed tangent action

  1. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.mfderiv_rotation_nilradical line 26
  2. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.mfderiv_rotation_cartan line 36
  3. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.mfderiv_individual_rotation line 45
  4. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotation_commutes_exponential line 64