OAI/Probability/SKGap/Terminal/ConsDiag.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.Noncrossing.Diagram.Paired.consDiag line 34
2. lemma OAI.SKGap.Noncrossing.Diagram.Paired.consDiag_bijective line 36
3. def OAI.SKGap.Noncrossing.Diagram.Paired.consDiagEquiv line 52
4. def OAI.SKGap.Noncrossing.Diagram.Paired.appendDiag line 54
5. lemma OAI.SKGap.Noncrossing.Diagram.Paired.appendDiag_bijective line 56
6. def OAI.SKGap.Noncrossing.Diagram.Paired.appendDiagEquiv line 65
7. instance OAI.SKGap.Noncrossing.Diagram.pairedNilUnique line 67
8. lemma OAI.SKGap.Noncrossing.Diagram.expect_nil line 75
9. lemma OAI.SKGap.Noncrossing.Diagram.expect_cons_diag line 78
10. lemma OAI.SKGap.Noncrossing.Diagram.expect_append_diag line 86
11. lemma OAI.SKGap.Noncrossing.WordSeries.ordinary_nil line 98
12. lemma OAI.SKGap.Noncrossing.WordSeries.ordinary_cons_diag line 99
13. lemma OAI.SKGap.Noncrossing.WordSeries.ordinary_append_diag line 101
14. lemma OAI.SKGap.Noncrossing.WordSeries.ordinary_diag_prefix line 104
15. lemma OAI.SKGap.Noncrossing.WordSeries.ordinary_diag_suffix line 109
16. lemma OAI.SKGap.Noncrossing.WordSeries.inverseCoefficient_diagonal line 116