OAI/GroupTheory/PolycyclicRecognition/Geometry/JordanLangTransversal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Lang transversals for commuting semisimple and unipotent factors

  1. theorem OAI.PolycyclicRecognition.jordan_lang_transversal_bijective line 14
  2. theorem OAI.PolycyclicRecognition.jordan_lang_decomposition line 49