mathlib

ad3e6672 - feat(order/chain): Flags (#13089)

feat(order/chain): Flags (#13089) Define the type of maximal chains, aka flags, of an order. Co-authored-by: Violeta Hernández <[vi.hdz.p@gmail.com](mailto:vi.hdz.p@gmail.com)>