OAI/Probability/BinarySweep/Representations/IrrepSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Irrep.invariant_eq_zero_of_finrank_gt_one line 16
2. lemma OAI.BinaryCoordinateSweeps.Irrep.sum_apply_eq_zero_of_finrank_gt_one line 32
3. lemma OAI.BinaryCoordinateSweeps.Irrep.sum_eq_zero_of_finrank_gt_one line 40
4. lemma OAI.BinaryCoordinateSweeps.Irrep.finrank_le_card line 47