OAI/GroupTheory/PolycyclicRecognition/Algebra/GeneratedUnipotentAction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A finite nilpotent action filtration from unipotent abelian generators

  1. theorem OAI.PolycyclicRecognition.action_filtration_preserved_of_commute line 13
  2. theorem OAI.PolycyclicRecognition.unipotent_generated_abelian_action_filtration line 33