OAI/NumberTheory/DukePrimeDegree/Entropy/WholeFutureEntropyCriterion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sublinear terminal-future name bounds force zero predecessor information

  1. theorem OAI.DukePrimeDegree.predecessor_information_zero_of_sublinear_words line 14