OAI/NumberTheory/DukePrimeDegree/Geometry/FiniteProductShear.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A coordinate shear of a finite root-product measure

  1. def OAI.DukePrimeDegree.finiteCoordinateEquiv line 13
  2. def OAI.DukePrimeDegree.finiteCoordinateShear line 17
  3. theorem OAI.DukePrimeDegree.finiteCoordinateShear_preserves line 22
  4. lemma OAI.DukePrimeDegree.finiteCoordinateShear_apply_same line 37
  5. lemma OAI.DukePrimeDegree.finiteCoordinateShear_apply_succAbove line 44