OAI/GroupTheory/PolycyclicRecognition/Geometry/SmoothRotationalAction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Joint smoothness of the compact action along a smooth representation

  1. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.action_factor_eq line 32
  2. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.contMDiff_action_factor line 45
  3. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.contMDiff_action_fixed line 60
  4. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.contMDiff_action_parameters line 75
  5. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.contMDiff_translated_action_parameters line 96
  6. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.contMDiffAt_translated_action line 106
  7. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.contMDiff_action line 118