OAI/NumberTheory/DukePrimeDegree/Geometry/TransverseRootFibers.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transverse coordinates of actual right root displacements

The transverse coordinate is constant on a right upper-unipotent leaf. A right diagonal displacement translates its logarithmic diagonal exactly. These identities allow return refinements to use transverse cells only.

  1. theorem OAI.DukePrimeDegree.transverse_eq_of_right_upperRoot line 18
  2. theorem OAI.DukePrimeDegree.transverse_eq_of_right_diagonal_upperRoot line 30
  3. theorem OAI.DukePrimeDegree.transverseLogDiagonal_right_diagonal_upperRoot line 51