OAI/GroupTheory/PolycyclicRecognition/Lattices/NilshadowRealAction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The real nilshadow action preserves the actual height

The logarithms vanish on the fixed quotient section. Commutation with its projection therefore forces the complete real action to preserve height, not merely its integral-time values.

  1. theorem OAI.PolycyclicRecognition.IntegralNilshadowData.exists_real_action line 23