mathlib

9134a8e7 - feat(combinatorics/simple_graph/hasse): Hasse diagram and path graph (#13959)

feat(combinatorics/simple_graph/hasse): Hasse diagram and path graph (#13959) Define the Hasse diagram of an order and the path graph on `n` vertices as the Hasse diagram of `fin n`.