OAI/Combinatorics/MatchingPSD/MatchingIncidence.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.MatchingSmoothing.Pairing.(instance at line 12) line 12
2. instance OAI.MatchingSmoothing.Pairing.relabelMulAction line 14
3. lemma OAI.MatchingSmoothing.Pairing.smul_eq_relabel line 20
4. def OAI.MatchingSmoothing.Pairing.table line 22
5. lemma OAI.MatchingSmoothing.Pairing.table_relabel line 26
6. def OAI.MatchingSmoothing.standardPairing line 43
7. lemma OAI.MatchingSmoothing.standardPairing_table line 49
8. def OAI.MatchingSmoothing.tableRelation line 77
9. def OAI.MatchingSmoothing.coloringPerm line 81
10. lemma OAI.MatchingSmoothing.commonIncidence_table_relabel line 89
11. lemma OAI.MatchingSmoothing.commonIncidence_standard line 103
12. lemma OAI.MatchingSmoothing.matching_table_trace_square line 119