OAI/NumberTheory/DukePrimeDegree/Geometry/NeutralGraphLifts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Identify small future lifts inside a neutral graph patch

  1. theorem OAI.DukePrimeDegree.neutral_graph_quotient_lift line 13
  2. theorem OAI.DukePrimeDegree.neutral_graph_small_future_lift line 41