OAI/Combinatorics/MatchingPSD/FiniteFactorization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PerfectMatchingPSD.endpoint_count line 9
2. lemma OAI.PerfectMatchingPSD.cut_degree_identity line 38
3. lemma OAI.PerfectMatchingPSD.crossingCount_pos line 53
4. lemma OAI.PerfectMatchingPSD.slack_nonneg line 59
5. lemma OAI.PerfectMatchingPSD.exists_diagonal_factorization line 69
6. lemma OAI.PerfectMatchingPSD.factor_orders_nonempty line 104
7. lemma OAI.PerfectMatchingPSD.psdRank_pos line 109
8. lemma OAI.PerfectMatchingPSD.hasFactorization_psdRank line 112
9. lemma OAI.PerfectMatchingPSD.psdRank_le line 115