OAI/GroupTheory/PolycyclicRecognition/Geometry/FactorPhaseDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The infinitesimal character of the actual Cartan factorization

  1. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.inverse_rotationCharacter_exp_line line 24
  2. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.hasDerivAt_inverse_factorPhase_line line 36
  3. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.mfderiv_inverse_factorPhase_apply line 55