Commit 2021-12-15 19:58 026e6929
View on Github →chore(combinatorics/simple_graph): fix name mixup (#10785) Fixes the name mixup from #10778 and reorders lemmas to make the difference more clear.
chore(combinatorics/simple_graph): fix name mixup (#10785) Fixes the name mixup from #10778 and reorders lemmas to make the difference more clear.