OAI/NumberTheory/DukePrimeDegree/Geometry/RemainingChainExistence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Completing a remaining-root chart from any initial pattern

  1. theorem OAI.DukePrimeDegree.exists_complete_chain_from_pattern line 12
  2. lemma OAI.DukePrimeDegree.EliminationChain.eq_done_of_completed line 43