OAI/Probability/SignedSweeps/PairConstituents.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.tensor_isotypic_zero line 16
2. lemma OAI.SignedSweeps.exists_tensor_isotypic_nonzero line 46
3. lemma OAI.SignedSweeps.tensor_map_equiv_nonzero line 58
4. def OAI.SignedSweeps.pairEmbeddingHom line 77
5. lemma OAI.SignedSweeps.pair_internal_intertwining line 81
6. lemma OAI.SignedSweeps.pair_projection_detects line 109
7. lemma OAI.SignedSweeps.pair_sector_adjoint_nonzero line 143
8. theorem OAI.SignedSweeps.pair_sector_constituent_occurrence line 159