OAI/Probability/SignedSweeps/PolytabloidNonzero.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.mem_row_col_eq_one line 11
2. lemma OAI.SignedSweeps.column_row_product_eq_one_iff line 20
3. lemma OAI.SignedSweeps.polytabloid_at_one line 38
4. lemma OAI.SignedSweeps.polytabloid_ne_zero line 46
5. def OAI.SignedSweeps.spechtGenerator line 51
6. lemma OAI.SignedSweeps.spechtGenerator_ne_zero line 54
7. instance OAI.SignedSweeps.spechtNontrivial line 59
8. lemma OAI.SignedSweeps.spechtDimension_pos line 62