OAI/NumberTheory/TotientAsymptotic/PrefixRecovery.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The head, common inner prefix and suffix determine a tuple exactly.

  1. lemma OAI.TotientAsymptotic.tuple_recovered_from_parts line 12
  2. lemma OAI.TotientAsymptotic.tupleValue_split_inner_suffix line 37