Theorem Finset.gc_map_inr_toRight

Modification history

2025-03-31 14:24
Mathlib/Data/Finset/Sum.lean
feat(Finset): extra `toLeft`/`toRight` API (#23020) …
Added Finset.gc_map_inr_toRightView on Github →