OAI/Probability/BinarySweep/YoungTheory/HookHilbertOccurrence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Young.hookHilbertMap line 15
2. lemma OAI.BinaryCoordinateSweeps.Young.hookHilbertMap_injective line 43
3. lemma OAI.BinaryCoordinateSweeps.Young.hookHilbert_occurs line 48
4. def OAI.BinaryCoordinateSweeps.Young.hookHilbertMapAt line 65
5. lemma OAI.BinaryCoordinateSweeps.Young.hookHilbertMapAt_injective line 93
6. lemma OAI.BinaryCoordinateSweeps.Young.hookHilbert_occursAt line 98