OAI/NumberTheory/DukePrimeDegree/Geometry/SparseUpperRootComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Sparse fine returns remove the transverse part of a future lift

  1. lemma OAI.DukePrimeDegree.homeomorph_pow_apply_eq_iterate line 15
  2. lemma OAI.DukePrimeDegree.diagonal_iterate_lift line 23
  3. theorem OAI.DukePrimeDegree.exists_sparse_upperRoot_comparison line 35
  4. theorem OAI.DukePrimeDegree.exists_conull_future1_root_relation line 126