OAI/NumberTheory/DukePrimeDegree/Dynamics/VelocityCommutant.lean

The commutant of a block-supported actual velocity space

An element of a subgroup always conjugates its own velocity space to itself. Once that space has the block support found by recurrence and contains the within-block root directions, its commutant is the block scalar algebra (when no block is a singleton). This gives the full normalizer conclusion directly, without assuming that the subgroup is normalized by the diagonal group or invoking a Lie subgroup theorem.