OAI/GroupTheory/PolycyclicRecognition/Algebra/KernelProductCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local multiplication coordinates for an integrated height kernel

The kernel inclusion and a normalized height section have complementary actual differentials. Their product map is therefore a local coordinate map at the identity, by the ordinary inverse function theorem.

  1. theorem OAI.PolycyclicRecognition.kernel_product_local_coordinates line 27