OAI/Probability/SwitchChain/BinaryColumnPartitions.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem315.BinaryColumnPartitions.Column line 10
2. def OAI.Problem315.BinaryColumnPartitions.unitColumn line 12
3. def OAI.Problem315.BinaryColumnPartitions.complementColumn line 17
4. lemma OAI.Problem315.BinaryColumnPartitions.column_one_surjective line 20
5. lemma OAI.Problem315.BinaryColumnPartitions.column_one_injective line 23
6. def OAI.Problem315.BinaryColumnPartitions.oneColumnEquiv line 26
7. def OAI.Problem315.BinaryColumnPartitions.complementEquiv line 29
8. def OAI.Problem315.BinaryColumnPartitions.twoColumnEquiv line 39
9. abbrev OAI.Problem315.BinaryColumnPartitions.MatrixSpace line 43
10. def OAI.Problem315.BinaryColumnPartitions.matrixEquiv line 48
11. theorem OAI.Problem315.BinaryColumnPartitions.matrixEquiv_inl line 74
12. theorem OAI.Problem315.BinaryColumnPartitions.matrixEquiv_inr line 77
13. theorem OAI.Problem315.BinaryColumnPartitions.row_sum_add line 84
14. def OAI.Problem315.BinaryColumnPartitions.fixedMarginsEquiv line 111
15. theorem OAI.Problem315.BinaryColumnPartitions.row_eq_iff line 126