Commit 2025-02-13 20:21 12ceac2a

View on Github →

chore(Data/Finset): avoid importing Group in Finset.Image (#21823) This PR is a step on the way to completely removing algebra from the dependencies of measure theory. It reverses the import direction Finset.Image -> Finset.Union and splits off some naturals-specific lemmas from Finset.Image.

Estimated changes

added theorem Finset.range_add
deleted theorem Finset.biUnion_image
deleted theorem Finset.biUnion_singleton
deleted theorem Finset.disjiUnion_map
deleted theorem Finset.image_biUnion
deleted theorem Finset.map_disjiUnion
deleted theorem Finset.range_add
added theorem Finset.biUnion_image
added theorem Finset.disjiUnion_map
added theorem Finset.image_biUnion
added theorem Finset.map_disjiUnion