OAI/GroupTheory/PolycyclicRecognition/Algebra/SemisimpleMovingAction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Equivariance of the centralizer product decomposition

  1. theorem OAI.PolycyclicRecognition.lieEquiv_map_ad_eq_zero line 14
  2. theorem OAI.PolycyclicRecognition.commuting_lieEquiv_preserves_movingCenter line 23
  3. theorem OAI.PolycyclicRecognition.commuting_lieEquiv_preserves_innerCentralizer line 35
  4. theorem OAI.PolycyclicRecognition.semisimple_projection_commutes line 43
  5. def OAI.PolycyclicRecognition.semisimpleMovingGroupAction line 53
  6. def OAI.PolycyclicRecognition.innerCentralizerGroupAction line 61
  7. theorem OAI.PolycyclicRecognition.movingGroupProjection_equivariant line 69