OAI/NumberTheory/DukePrimeDegree/Geometry/RootFiberConstancy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Leaf constancy on the remaining-coordinate fibers

With the selected root last in the product coordinates, different remaining coordinates are related by a conjugate of the remaining group. Its normality and neutral holonomy therefore give equality of the actual normalized root leaves on each such coordinate fiber.

  1. theorem OAI.DukePrimeDegree.remaining_root_conjugate_mem line 21
  2. theorem OAI.DukePrimeDegree.exists_nullset_remaining_root_fiber_constancy line 39