Commit 2025-02-16 17:03 877ab3f2
View on Github →RFC: generalize Disjoint.map (#20839)
xy: I wanted to have Disjoint.map generalize the mpr part of Finset.disjoint_map,
so that Finpartition.map can be generalized to something that includes Finset.map.
I'm no longer sure that I'll need this for the larger goal, so it's OK to just reject this PR.