mathlib3

662786a8 - refactor(data/{finite,fintype}): redefine `infinite` in terms of `finite`, move to `data.finite.defs` (#16390)