OAI/Probability/BinarySweep/Representations/IsotypicMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Irrep.groupAverage line 18
2. def OAI.BinaryCoordinateSweeps.Irrep.evenMoment line 20
3. lemma OAI.BinaryCoordinateSweeps.Irrep.unitary_rep_adjoint line 24
4. lemma OAI.BinaryCoordinateSweeps.Irrep.average_compatible line 36
5. lemma OAI.BinaryCoordinateSweeps.Irrep.adjoint_average_compatible line 41
6. lemma OAI.BinaryCoordinateSweeps.Irrep.even_compatible line 49
7. theorem OAI.BinaryCoordinateSweeps.Irrep.multiplicity_moment_le line 61