OAI/Probability/BinarySweep/YoungTheory/YoungAnti.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Young.signC line 12
2. lemma OAI.BinaryCoordinateSweeps.Young.signC_eq line 15
3. lemma OAI.BinaryCoordinateSweeps.Young.signC_sq line 17
4. lemma OAI.BinaryCoordinateSweeps.Young.signC_ne_zero line 22
5. lemma OAI.BinaryCoordinateSweeps.Young.signC_inv line 27
6. lemma OAI.BinaryCoordinateSweeps.Young.signC_swap line 31
7. abbrev OAI.BinaryCoordinateSweeps.Young.C line 34
8. instance OAI.BinaryCoordinateSweeps.Young.(instance at line 35) line 35
9. def OAI.BinaryCoordinateSweeps.Young.columnAnti line 37
10. lemma OAI.BinaryCoordinateSweeps.Young.columnAnti_apply line 40
11. lemma OAI.BinaryCoordinateSweeps.Young.columnAnti_rep line 44
12. def OAI.BinaryCoordinateSweeps.Young.polytabloid line 60
13. lemma OAI.BinaryCoordinateSweeps.Young.columnAnti_basis_column line 63
14. lemma OAI.BinaryCoordinateSweeps.Young.col_fixes_base_iff line 68
15. lemma OAI.BinaryCoordinateSweeps.Young.polytabloid_base line 83
16. lemma OAI.BinaryCoordinateSweeps.Young.polytabloid_ne_zero line 92
17. lemma OAI.BinaryCoordinateSweeps.Young.swap_mem_fiber line 98
18. lemma OAI.BinaryCoordinateSweeps.Young.swap_fixes_tabloid line 103
19. lemma OAI.BinaryCoordinateSweeps.Young.columnAnti_basis_collision line 110
20. lemma OAI.BinaryCoordinateSweeps.Young.columnAnti_basis_span line 126
21. lemma OAI.BinaryCoordinateSweeps.Young.sum_tabloidBasis line 135
22. theorem OAI.BinaryCoordinateSweeps.Young.columnAnti_rank_one line 140
23. lemma OAI.BinaryCoordinateSweeps.Young.columnAnti_square line 155
24. lemma OAI.BinaryCoordinateSweeps.Young.columnAnti_polytabloid line 163