mathlib

c32efeae - feat(data/fin): there is at most one `order_iso` from `fin n` to `α` (#5499)

feat(data/fin): there is at most one `order_iso` from `fin n` to `α` (#5499) * Define a `bounded_lattice` instance on `fin (n + 1)`. * Prove that there is at most one `order_iso` from `fin n` to `α`.