Commit 2024-10-01 22:56 f1843eb9
View on Github →chore(Data/Finset): split lattice file (#17049) The file Data/Finset/Lattice contained two disjoint developments, with disjoint imports, forming one natural cut location. We also split max and min into a separate file.