Theorem List.getD_surjective_iff

Modification history

2025-11-05 02:43
Mathlib/Data/List/GetD.lean
feat(Data/List/GetD): `getD` is surjective iff every element is in the list (#30217)
Added List.getD_surjective_iffView on Github →