OAI/Probability/BinarySweep/Representations/IrrepTransport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Irrep.subrepresentationCongr line 11
2. lemma OAI.BinaryCoordinateSweeps.Irrep.irreducible_comp_equiv line 22
3. def OAI.BinaryCoordinateSweeps.Irrep.classCharacter line 28
4. lemma OAI.BinaryCoordinateSweeps.Irrep.classCharacter_mk line 34
5. def OAI.BinaryCoordinateSweeps.Irrep.classPairRight line 37
6. lemma OAI.BinaryCoordinateSweeps.Irrep.classPair_character_self line 47
7. lemma OAI.BinaryCoordinateSweeps.Irrep.classPair_characters line 54