OAI/NumberTheory/TwoPoint/Walks/AttachedResidueLift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One common integer realizes every attached numerical witness in a hybrid sample.

  1. theorem OAI.TwoPointCorrelations.attached_residue_words_common_origin line 12