OAI/GroupTheory/PolycyclicRecognition/Lattices/JointFixedActionFiltration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The residual quotient actions commute on lower-central factors

The two orders of quotient lifts differ by inner automorphisms. Intrinsic BCH commutator estimates make both inner corrections disappear on the next Lie lower-central quotient.

  1. theorem OAI.PolycyclicRecognition.jointFixed_action_preserves_lowerCentral line 21
  2. theorem OAI.PolycyclicRecognition.jointFixed_actions_commute_mod_lowerCentral line 29