mathlib3

937b1c59 - feat(order/category): Category of finite distributive lattices (#11677)

feat(order/category): Category of finite distributive lattices (#11677) Define `FinBddDistLat`, the category of finite distributive lattices with bounded lattice homomorphisms. This is one of the two categories involved in Birkhoff's representation theorem.