OAI/GroupTheory/PolycyclicRecognition/Geometry/UnipotentCoordinateBCH.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The universal product formula in faithful unipotent coordinates

This algebraic transport uses only the exponential compatibility of the given representation. Its bound may be enlarged, so two coordinate models can use exactly the same coefficients.

  1. theorem OAI.PolycyclicRecognition.finite_product_of_unipotent_coordinates line 22