mathlib

bcf5b1a6 - feat(data/fintype/basic): to_finset lattice lemmas (#7077)

feat(data/fintype/basic): to_finset lattice lemmas (#7077) While we do not have lattice homomorphisms, we can still provide some similar API. Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>