OAI/GroupTheory/PolycyclicRecognition/Algebra/ComplexFactorLocalChart.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Smooth local coordinates from the complex-weight factors

  1. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.kernelParameter line 25
  2. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.cartanParameter line 29
  3. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.factorParameter line 33
  4. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.factorParameter_zero line 37
  5. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.contMDiff_factorParameter line 44
  6. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.factorParameter_line line 50
  7. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.hasMFDerivAt_factorParameter_line line 61
  8. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.hasMFDerivAt_factorParameter line 86
  9. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.exists_smooth_factorSection line 93