Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-21 01:43 d145e8e3

View on Github →

chore(combinatorics/simple_graph/basic): Golf and cleanup (#10942) This kills a few simp and fixes typos.

Estimated changes