Theorem Finset.biUnion_singleton

Modification history

2025-08-03 23:41

Mathlib/Data/Finset/Union.lean

feat: start adding `@[grind]` annotations for `Finset` (#27818) …

Modified Finset.biUnion_singleton View on Github →

2025-02-13 20:21

Mathlib/Data/Finset/Image.lean

chore(Data/Finset): avoid importing `Group` in `Finset.Image` (#21823) …

Modified Finset.biUnion_singleton View on Github →

2023-05-14 07:05

Mathlib/Data/Finset/Image.lean

chore: Rename to `sSup`/`iSup` (#3938) …

Added Finset.biUnion_singleton View on Github →