OAI/GroupTheory/PolycyclicRecognition/Algebra/MaximizingCoordinateCriterion.lean

The converse basis-exchange criterion

An invertible selected basis is maximizing if every nonzero coordinate of each available vector lies in a basis direction of at least its weight. The determinant permutation supplies the required matching for any rival basis. This is used to extend an ideal basis by zero-width pure words.