OAI/NumberTheory/DukePrimeDegree/Geometry/HorosphereIsolatedLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Peripheral root limits of diagonal conjugates

The isolating flows send any shearing-horosphere element to the transvection whose parameter is the selected matrix entry.

  1. theorem OAI.DukePrimeDegree.horosphere_isolated_root_limit line 19
  2. theorem OAI.DukePrimeDegree.horosphere_row_root_limit line 73
  3. theorem OAI.DukePrimeDegree.horosphere_column_root_limit line 85