Def Finset.toRight

Modification history

2025-03-31 14:24

Mathlib/Data/Finset/Sum.lean

feat(Finset): extra `toLeft`/`toRight` API (#23020) …

Modified Finset.toRight View on Github →

2024-10-04 10:12

Mathlib/Data/Finset/Sum.lean

feat(Data/Finset): right elements of a finset in the sum type (#17014)

Added Finset.toRight View on Github →