OAI/Combinatorics/MatchingPSD/EdgeMonomials.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingSmoothing.Pairing.edgeMonomial line 12
2. def OAI.MatchingSmoothing.Pairing.ContainsList line 15
3. def OAI.MatchingSmoothing.Pairing.edgeSupport line 18
4. lemma OAI.MatchingSmoothing.Pairing.mem_edgeSupport line 21
5. lemma OAI.MatchingSmoothing.Pairing.edgeMonomial_eq_indicator line 32
6. lemma OAI.MatchingSmoothing.Pairing.edgeMonomial_cons line 42
7. lemma OAI.MatchingSmoothing.Pairing.contains_partner_support line 46
8. lemma OAI.MatchingSmoothing.Pairing.contains_agree_support line 55
9. lemma OAI.MatchingSmoothing.Pairing.redundant_edgeMonomial line 63
10. lemma OAI.MatchingSmoothing.Pairing.edgeMonomial_zero_of_unsatisfiable line 80
11. lemma OAI.MatchingSmoothing.Pairing.edgeMonomial_act_fix line 86
12. def OAI.MatchingSmoothing.colorStabilizer line 104
13. def OAI.MatchingSmoothing.colorAverage line 110
14. lemma OAI.MatchingSmoothing.colorAverage_apply line 114
15. lemma OAI.MatchingSmoothing.colorAverage_act line 119
16. lemma OAI.MatchingSmoothing.colorAverage_one line 126
17. lemma OAI.MatchingSmoothing.colorAverage_mul_invariant line 130