mathlib
d145e8e3 - chore(combinatorics/simple_graph/basic): Golf and cleanup (#10942)

Commit
4 years ago
chore(combinatorics/simple_graph/basic): Golf and cleanup (#10942) This kills a few `simp` and fixes typos.
Author
Parents
Loading