OAI/NumberTheory/DukePrimeDegree/Geometry/NeutralAction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The neutral diagonal action on the lattice quotient

The concrete neutral weight subgroup acts continuously by right diagonal translations. Its measure-preserving action follows from full diagonal invariance, and every trace-zero neutral weight is represented in it.

  1. def OAI.DukePrimeDegree.neutralDiagonalAction line 20
  2. lemma OAI.DukePrimeDegree.neutralDiagonalAction_continuous line 25
  3. lemma OAI.DukePrimeDegree.neutralDiagonalAction_apply line 34
  4. lemma OAI.DukePrimeDegree.neutralDiagonal_preserving line 39
  5. lemma OAI.DukePrimeDegree.neutralDiagonal_apply_weights line 52