OAI/GroupTheory/PolycyclicRecognition/Lattices/JointFixedSubalgebra.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The joint fixed algebra and its unipotent quotient-lift actions

  1. def OAI.PolycyclicRecognition.jointFixedLieSubalgebra line 13
  2. theorem OAI.PolycyclicRecognition.mem_jointFixedLieSubalgebra line 28
  3. theorem OAI.PolycyclicRecognition.commuting_lieEquiv_preserves_jointFixed line 32
  4. def OAI.PolycyclicRecognition.jointFixedLinearAction line 40
  5. def OAI.PolycyclicRecognition.jointFixedLieAction line 45
  6. theorem OAI.PolycyclicRecognition.jointFixedLinearAction_unipotent line 58
  7. def OAI.PolycyclicRecognition.jointFixedGroupAction line 87