mathlib
026e6929 - chore(combinatorics/simple_graph): fix name mixup (#10785)

Commit

4 years ago

chore(combinatorics/simple_graph): fix name mixup (#10785) Fixes the name mixup from #10778 and reorders lemmas to make the difference more clear.

Author

b-mehta

Parents