OAI/Probability/BinarySweep/YoungTheory/YoungInducedMap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Young.tabloidVector line 17
2. lemma OAI.BinaryCoordinateSweeps.Young.tabloidVector_eq line 20
3. lemma OAI.BinaryCoordinateSweeps.Young.tabloidVector_smul line 32
4. def OAI.BinaryCoordinateSweeps.Young.fromTabloid line 39
5. lemma OAI.BinaryCoordinateSweeps.Young.fromTabloid_basis line 45
6. lemma OAI.BinaryCoordinateSweeps.Young.fromTabloid_intertwines line 49
7. lemma OAI.BinaryCoordinateSweeps.Young.spechtPoly_column line 60
8. lemma OAI.BinaryCoordinateSweeps.Signed.mask_ofSubtype line 93
9. lemma OAI.BinaryCoordinateSweeps.Signed.koszulSign_ofSubtype line 102
10. lemma OAI.BinaryCoordinateSweeps.Signed.mask_of_fixed_complement line 113
11. lemma OAI.BinaryCoordinateSweeps.Signed.mask_fixed_complement line 128
12. lemma OAI.BinaryCoordinateSweeps.Signed.koszulSign_of_fixed_complement line 139