OAI/Probability/SignedSweeps/Invariants.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedSweeps.complexSign line 11
2. lemma OAI.SignedSweeps.colSubgroup_has_odd line 16
3. lemma OAI.SignedSweeps.colSubgroup_sum_sign_eq_zero line 34
4. def OAI.SignedSweeps.regularSum line 45
5. lemma OAI.SignedSweeps.regularSum_single line 50
6. lemma OAI.SignedSweeps.regularSum_invariant line 55
7. lemma OAI.SignedSweeps.polytabloid_sum_eq_zero line 60
8. def OAI.SignedSweeps.spechtInclusion line 68
9. lemma OAI.SignedSweeps.spechtSum_eq_zero line 71
10. lemma OAI.SignedSweeps.specht_invariant_eq_zero line 80