OAI/GroupTheory/PolycyclicRecognition/Algebra/HigherExteriorFreeOrbitBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A high finite exterior power rules out a free polynomial orbit

The coefficient algebra is the actual acting group ring. Its finite algebra presentation bounds the independent coordinates detected by the determinant.

  1. theorem OAI.PolycyclicRecognition.higherExterior_free_orbit_bound line 21