mathlib

80e072ec - feat(data/finset/basic): random golf (#11576)