Commit 2025-09-06 11:10 66766944
View on Github →chore: Rename theorems involving finset_biUnion and similar (#29091)
Some theorems involving a biUnion indexed by a Finset were named using finset_biUnion and some were named using biUnion_finset. This PR adopts the consistent use of biUnion_finset, and similarly changes finset_biInter and fintype_iUnion. (There are no occurences of fintype_iInter.)