OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialModelHom.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Smooth homomorphisms in polynomial exponential coordinates are linear

  1. def OAI.PolycyclicRecognition.polynomialModelLieHom line 15
  2. theorem OAI.PolycyclicRecognition.polynomialModelLieHom_apply line 19
  3. def OAI.PolycyclicRecognition.polynomialModelLieEquiv line 33
  4. theorem OAI.PolycyclicRecognition.polynomialModelLieEquiv_apply line 41