OAI/NumberTheory/DukePrimeDegree/Entropy/LowEntropySupportReduction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Reduction of root invariance to the published support lemma

For the integer-lattice quotient, exclusion of exceptional neutral returns and the shearing argument give root invariance from the support conclusion of EKL (2006), Lemma 4.4(1).

  1. theorem OAI.DukePrimeDegree.root_invariant_of_horospherical_root_support line 20