OAI/GroupTheory/PolycyclicRecognition/Algebra/EndomorphismCommutatorFiltration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The commutator-filtration bridge for linear endomorphism representations

  1. theorem OAI.PolycyclicRecognition.linearActionFiltration_comp_le line 12
  2. theorem OAI.PolycyclicRecognition.relativeCommutatorSeries_le_endFiltration line 23
  3. theorem OAI.PolycyclicRecognition.relativeCommutatorSeries_le_kernel_of_endFiltration line 52