OAI/Probability/SignedSweeps/CoefficientAlgebra.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedSweeps.coefficientProduct line 11
2. def OAI.SignedSweeps.coefficientStar line 13
3. def OAI.SignedSweeps.coefficientOne line 15
4. lemma OAI.SignedSweeps.coefficientAction_mul line 28
5. lemma OAI.SignedSweeps.coefficientAction_one line 44
6. lemma OAI.SignedSweeps.coefficientAction_commute line 49
7. lemma OAI.SignedSweeps.coefficientAction_star line 54
8. theorem OAI.SignedSweeps.trace_product_specht_expansion line 65
9. lemma OAI.SignedSweeps.specht_positive_coefficient_product line 75
10. lemma OAI.SignedSweeps.multiplicity_term_le_sum line 87
11. theorem OAI.SignedSweeps.multiplicity_positive_product_trace line 95