OAI/GroupTheory/PolycyclicRecognition/Geometry/JordanTransversalLinearMap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The invertible leading term for a general Jordan Lang transversal

Only the moving part of the semisimple operator is inverted. Its commuting unipotent factor is a nilpotent perturbation of this invertible leading term.

  1. theorem OAI.PolycyclicRecognition.jordan_transversal_linear_bijective line 17