OAI/NumberTheory/OrdinaryCorrelations/HighTrace/BelowChain.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.Rerooting.BelowChain line 18
2. def OAI.OrdinaryCorrelations.Rerooting.rank line 21
3. lemma OAI.OrdinaryCorrelations.Rerooting.rank_realized line 25
4. lemma OAI.OrdinaryCorrelations.Rerooting.rank_lt line 32
5. theorem OAI.OrdinaryCorrelations.Rerooting.chain_or_antichain line 50
6. def OAI.OrdinaryCorrelations.Rerooting.Chain line 82
7. def OAI.OrdinaryCorrelations.Rerooting.Anti line 84
8. lemma OAI.OrdinaryCorrelations.Rerooting.chain_or_antichain_subset line 88
9. lemma OAI.OrdinaryCorrelations.Rerooting.Chain.mono line 114
10. lemma OAI.OrdinaryCorrelations.Rerooting.Anti.mono line 117
11. def OAI.OrdinaryCorrelations.Rerooting.Agree line 120
12. def OAI.OrdinaryCorrelations.Rerooting.Reverse line 122
13. lemma OAI.OrdinaryCorrelations.Rerooting.reverse_of_two_chains line 125
14. theorem OAI.OrdinaryCorrelations.Rerooting.two_order_extraction line 138