OAI/GroupTheory/PolycyclicRecognition/Lattices/NilshadowWeightAction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The original solvable algebra as an extension of its nilshadow

  1. theorem OAI.PolycyclicRecognition.heightSemisimpleAction_apply_commute line 20
  2. theorem OAI.PolycyclicRecognition.cartanNilshadow_bracket_symm line 24
  3. theorem OAI.PolycyclicRecognition.semisimple_derives_nilshadow_bracket line 31
  4. def OAI.PolycyclicRecognition.nilshadowWeightOperator line 41
  5. theorem OAI.PolycyclicRecognition.nilshadowWeightOperator_symm line 45
  6. def OAI.PolycyclicRecognition.nilshadowWeightDerivation line 49
  7. theorem OAI.PolycyclicRecognition.nilshadowWeightDerivation_symm line 60
  8. theorem OAI.PolycyclicRecognition.nilshadowWeightDerivation_equiv line 64
  9. def OAI.PolycyclicRecognition.nilshadowWeightAction line 69
  10. def OAI.PolycyclicRecognition.nilshadowSemidirectEmbedding line 91
  11. theorem OAI.PolycyclicRecognition.nilshadowSemidirectEmbedding_injective line 114