OAI/Probability/SignedSweeps/InvariantObstruction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedSweeps.supportedSubgroup line 12
2. lemma OAI.SignedSweeps.swap_mem_supportedSubgroup line 23
3. lemma OAI.SignedSweeps.Partition.colOf_lt_firstRow line 29
4. lemma OAI.SignedSweeps.large_set_column_pair line 35
5. lemma OAI.SignedSweeps.supportedAverage_annihilates_generator line 48
6. lemma OAI.SignedSweeps.supportedAverage_eq_zero line 66
7. lemma OAI.SignedSweeps.specht_supported_invariant_eq_zero line 87
8. lemma OAI.SignedSweeps.specht_right_supported_sum_eq_zero line 95