OAI/GroupTheory/PolycyclicRecognition/Analysis/NormalInductionSupport.lean

Supports of rank-one vectors in an induced representation

For induction from a normal subgroup, the quotient acts transitively on the coordinate positions. A rank-one subrepresentation must therefore have either empty support or every quotient coordinate in its support.