OAI/NumberTheory/DukePrimeDegree/Geometry/TransverseDiagonalFactorization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact neutral fibers of the transverse coordinate map

On the positive-diagonal chart, equality of column ratios means that two transverse points differ by an actual positive diagonal matrix. This identifies the neutral coordinates without an abstract quotient factor.

  1. lemma OAI.DukePrimeDegree.upperRootTransverse_diagonal_prod line 18
  2. lemma OAI.DukePrimeDegree.transverse_positive_same_ratios_iff line 23
  3. lemma OAI.DukePrimeDegree.transverse_positive_same_ratios_neutral line 53