OAI/NumberTheory/DukePrimeDegree/Entropy/RootPredecessorWords.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-word root information in the ambient predecessor alphabet

  1. theorem OAI.DukePrimeDegree.labeled_kernel_information line 13
  2. theorem OAI.DukePrimeDegree.EliminationChain.predecessor_word_root_information line 33