OAI/GroupTheory/PolycyclicRecognition/Algebra/AlternatingPolynomialCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial and smooth coordinates for the alternating product

These coordinates keep the two embedding maps among the coefficient parameters. The input chart can be any fixed continuous linear equivalence.

  1. theorem OAI.PolycyclicRecognition.hasPolynomialCoordinates_linear line 16
  2. abbrev OAI.PolycyclicRecognition.AlternatingLawData line 35
  3. def OAI.PolycyclicRecognition.flatAlternatingProduct line 39
  4. theorem OAI.PolycyclicRecognition.hasPolynomialCoordinates_flatAlternatingProduct line 44
  5. theorem OAI.PolycyclicRecognition.contDiff_flatAlternatingProduct line 59
  6. theorem OAI.PolycyclicRecognition.flatAlternatingProduct_submersive line 77