OAI/NumberTheory/OrdinaryCorrelations/HighTrace/MemTakeIndex.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.Rerooting.mem_take_index line 19
2. def OAI.OrdinaryCorrelations.Rerooting.leftGate line 27
3. lemma OAI.OrdinaryCorrelations.Rerooting.Gate.path_unique line 39
4. lemma OAI.OrdinaryCorrelations.Rerooting.leftGate_length line 44
5. lemma OAI.OrdinaryCorrelations.Rerooting.rightGate_length line 50
6. lemma OAI.OrdinaryCorrelations.Rerooting.ancestor_length_lt line 56
7. lemma OAI.OrdinaryCorrelations.Rerooting.gate_dependency line 63