mathlib

57c6d191 - feat(combinatorics/simple_graph): finitely many simple graphs on a finite type (#5584)

feat(combinatorics/simple_graph): finitely many simple graphs on a finite type (#5584) Adds an `ext` lemma for simple graphs and an instance that there are finitely many if the vertex set is finite.