Commit 2025-11-05 02:43 fc2363bf

View on Github →

feat(Data/List/GetD): getD is surjective iff every element is in the list (#30217)

Estimated changes

added theorem List.getD_surjective