OAI/NumberTheory/DukePrimeDegree/Geometry/CommutatorInvariance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Invariance under a commutator root

Two nonatomic adjacent root conditionals force invariance under the long root. This proves EKL (2006), Lemma 3.3 / Einsiedler–Katok (2003), Lemma 6.1, for the arithmetic quotient. Every vertex is selected outside a common leafwise saturated null set.

  1. lemma OAI.DukePrimeDegree.exists_nonzero_parameter_of_ae line 22
  2. theorem OAI.DukePrimeDegree.root_invariant_of_adjacent_nonatomic_leaves line 34