OAI/NumberTheory/DukePrimeDegree/Dynamics/UnipotentFreeness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Freeness of the full positive unipotent action

At the generic lattices already supplied by diagonal recurrence, no nonzero lattice vector has a zero coordinate. A stabilizer element with one identity column must therefore fix every lattice vector, so is the identity. In particular all positive-root groups act freely there, simultaneously.

  1. theorem OAI.DukePrimeDegree.positiveRootPattern_stabilizer_trivial line 22
  2. theorem OAI.DukePrimeDegree.ae_positiveRootPattern_stabilizer_trivial line 33