OAI/NumberTheory/DukePrimeDegree/Geometry/IteratedRootShear.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite compositions of the elementary remaining-root shears

  1. def OAI.DukePrimeDegree.iteratedCoordinateShear line 12
  2. lemma OAI.DukePrimeDegree.iteratedCoordinateShear_apply_outside line 17
  3. lemma OAI.DukePrimeDegree.iteratedCoordinateShear_apply line 29
  4. theorem OAI.DukePrimeDegree.iteratedCoordinateShear_preserves line 51