OAI/NumberTheory/DukePrimeDegree/Geometry/AtomicRootLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Atomic root leaves exclude nonzero diagonal limits

Compact simultaneous recurrence converts any root limit of diagonal conjugates into two points on one root orbit in an atomic transversal. Consequently the root parameter must vanish. Only invariance under the diagonal group and atomicity of the specified root are used.

  1. theorem OAI.DukePrimeDegree.exists_nullset_atomic_root_limit line 24